Software Development based on Models and Constraints

2018 Fiscal Year Final Research Report

• Project/Area Number: 16K00094
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Shinshu University
• Principal Investigator: OKANO KOZO 信州大学, 学術研究院工学系, 准教授 (70252632)
• Co-Investigator(Kenkyū-buntansha): 関澤 俊弦 日本大学, 工学部, 准教授 (10549314) ; 小形 真平 信州大学, 学術研究院工学系, 助教 (10589279)
• Project Period (FY): 2016-04-01 – 2019-03-31
• Keywords: 仕様記述 / 検証 / モデル

Outline of Final Research Achievements

We developed a tool to derive the state transitions from the requirement specification. Morphemes and parsing results are stored in XML format. The state transitions are derived from the specification description sentences of the "electric pot", and the state variables and the state transitions are successfully derived at a high recall rate. In addition, we proposed a method to determine similarity of class diagrams from class attributes, and developed a review support system where synthesized voice feedbacks the review results. We have proposed a behavioral equivalence verification method using SAW for a program using a recursive structure. We have also made presentations at safety analyzing methods integrated STAMP/STPA and model checking.

Free Research Field

ソフトウェア工学

Academic Significance and Societal Importance of the Research Achievements

自然語要求記述からコンピュータで解析できる動作モデルを自動導出できることを限定されたドメインと記述スタイルであれば可能であることを示した。またプログラムコードレベルでの比較的小さな機能単位である関数が異なったアルゴリズムで同一の計算をしている場合に、その関数がリストやバイナリツリーのような再帰データを扱うような複雑なものであっても網羅的に動作の等価性を限定されたサイズ内で全自動で調べることはできることを示した。またこのようなモデル検査をSTAMP/STPAという安全検査手法と結びつける成果を一部提供できた。