2020 Fiscal Year Research-status Report
実現可能性必要条件に基づいた協調的リアクティブシステム自動合成
| Project/Area Number |
17K17763
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
冨田 尭 北陸先端科学技術大学院大学, 情報社会基盤研究センター, 講師 (80749226)
|
|---|
| Project Period (FY) |
2017-04-01 – 2022-03-31
|
| Keywords | ソフトウェア工学 / ソフトウェア検証 / 形式手法 / 協調的リテクティブシステム / 実現可能性 / 自動合成 |
|---|
| Outline of Annual Research Achievements |
仕様からのリアクティブシステムの自動合成では，通常，仕様違反させようとする敵対的環境を想定することで，非常に強い信頼性と安全性をもつリアクティブシステムの合成を試みるが，現実には，環境とリアクティブシステムの関係は必ずしも敵対的ではなく，協調・共生を前提とすることも多い．本研究では仕様の実現可能性必要条件に基づき協調的リアクティブシステムを自動合成する手法の開発を目的とし，関連研究の調査を行い，また，研究中に見出した実現可能性必要条件群及び既知の実現可能性必要条件群の厳密な形式的定義を呼び階層定理群を与えた．これらの実現可能性必要条件群は網羅性，保存可能性，安定化可能性及び戦略化可能性の4つの観点から体系的・階層的に分類でき，その観点から協力が発生し得ることを導くことができる．例えば，安定化可能性（相手からの一時的な協力により恒久的な安定状態へ到達し仕様を満たすことができるという性質）の観点からは，リアクティブシステム及び環境のそれぞれの目的（仕様）がそれぞれの立場から安定化可能であり，かつ，それぞれの安定状態へ到達するまでのお互いのふるまいが矛盾しないのであれば，システムを環境が協調することでそれぞれの目的（仕様）を満足することが可能となることが導出できる．また，保存可能性（仕様の充足可能性を保持し続けることができるという性質）の観点からも，類似の協調が発生する可能性を導出できる．ただし，必然的あるいは妥協的な協調が発生するための必要充分な条件を見出すには至っていない．令和2年度は，実現可能性必要条件群の特性について，判定手続きを構成するサブルーチンの共通性及び類似性からも分析し，また，各実現可能性必要条件判定の計算量を導出した．
|
| Current Status of Research Progress |
Current Status of Research Progress
4: Progress in research has been delayed.
Reason
実現可能性必要条件に基づいてリアクティブシステム-環境間の協調発生条件の特徴付けを試みたものの，必然的あるいは妥協的な協調強調が発生する必要充分 な条件を見出すには至らなかった．また，これまでに発見したものを含め実現可能性必要条件群の特性及び計算量の分析，特に判定手続きの構成から見た実現可能性必要条件群の分析を優先して行なったため，当初の既知実現可能性必要条件群に基づいた協調的リアクティブシステム自動合成手法の開発及びその技術的課題を充分に明らかにすることはできなかった．そして，コロナ禍において所属部署（情報社会基盤研究センター）の業務が大幅に増加したため，当初の予定通りにエフォートを割くことができなかったため，成果のすべてを論文にまとめることができなかった．
|
| Strategy for Future Research Activity |
今後は，これまでの成果をもとに実現可能性必要条件群に基づいてシステムと環境間で必然的あるいは妥協的に協調が発生する条件について詳細な分析を行い，その時に不完全/協調的リアクティブシステムを自動合成する手法の開発を目指す．また，その際に，従来の自動合成技術のうち，協調関係を考慮しても上手く機能する技術及び考慮するが故に上手く機能しない技術について分析し，新しい技術の開発にも取り組む．そして，従来型の敵対的環境を想定した実現可能性必要条件に基づいた協調的実現可能性ではなく，非敵対的環境を想定した協調的実現可能性の直接的な特徴付け及びそれに基づいた協調的リアクティブシステム自動合成手法，更には，協調関係を考慮した上での仕様欠陥分析・抽出手法等の関連技術の開発も試みる．
|
| Causes of Carryover |
研究進捗の遅れのため．
再延長年度における国際会議及び国内会議参加のための旅費，プログラム実装のための人件費・謝金，その他学会参加費や論文掲載料等に用いる.
|
Research Products
(1 results)
