| Project/Area Number |
17K17763
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Computer system
Software
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
Tomita Takashi 北陸先端科学技術大学院大学, 情報社会基盤研究センター, 講師 (80749226)
|
|---|
| Project Period (FY) |
2017-04-01 – 2023-03-31
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2019: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2018: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2017: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | ソフトウェア工学 / ソフトウェア検証 / 形式手法 / 協調的リアクティブシステム / 実現可能性 / 自動合成 / 協調的リテクティブシステム |
|---|
| Outline of Final Research Achievements |
In this research, we tackled the development of an automatic synthesis method of a cooperative reactive system from a formal requirement specification, based on necessary conditions of realizability of the specification.
We found eight new necessary conditions of the realizability, gave a systematic characterization for the new conditions and also existing ones, and proof a hierarchy theorem among the conditions. The conditions are systematically categorized with four viewpoints: exhaustivity, strategizability, preservability and stability. In these viewpoints, we can analyze defects of specifications and also imply the possibility of cooperation between a reactive system and external environment. We also revealed expected complexities of checking problems for the necessary conditions, based on the similarity among subroutines of their checking procedures. That is, we established the basis of cooperative reactive system synthesis methods based on necessary conditions of realizability.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究成果は，より現実的・一般的な自動合成技術の基盤を与えたという点で学術的・社会的な意義がある．
古典的なリアクティブシステム自動合成では敵対的な環境を想定するという過度に厳しい安全性に基づいていたが，本研究では協調の発生を想定し緩和された安全性に基づく自動合成に注目し，合成可能性の基盤となる実現可能性必要条件群について分析した．その結果，実現可能性必要条件群の判定手続きの期待計算量は大きいものの，体系的な特徴付け・分類により，要求仕様の欠陥や協調不調についてのより詳細な分析が可能なことが明らかになったため，仕様修正の容易化を期待できる．
|
