Software Development based on Models and Constraints
| 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
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2018: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2017: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2016: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Keywords | 仕様記述 / 検証 / モデル / ソフトウェア工学 / 仕様記述解析 / NLP / 形態素解析 / 自然語解析 / 要求仕様書 / 状態遷移 / 構文解析 / 機械学習 / 要求仕様 / 形式記述 / オートマトン / モデル検査 / CYKアルゴリズム / ソフトウエア学 / 制約指向 |
|---|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
自然語要求記述からコンピュータで解析できる動作モデルを自動導出できることを限定されたドメインと記述スタイルであれば可能であることを示した。またプログラムコードレベルでの比較的小さな機能単位である関数が異なったアルゴリズムで同一の計算をしている場合に、その関数がリストやバイナリツリーのような再帰データを扱うような複雑なものであっても網羅的に動作の等価性を限定されたサイズ内で全自動で調べることはできることを示した。またこのようなモデル検査をSTAMP/STPAという安全検査手法と結びつける成果を一部提供できた。
|
Report
(4 results)
Research Products
(4 results)
