2021 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 – 2023-03-31
|
| Keywords | ソフトウェア工学 / ソフトウェア検証 / 形式手法 / 協調的リアクティブシステム / 実現可能性 / 自動合成 |
|---|
| Outline of Annual Research Achievements |
仕様からのリアクティブシステム（RS）の自動合成では，通常，仕様違反させようとする敵対的環境を想定することで，非常に強い信頼性と安全性をもつRSの合成を試みる．しかし現実には，環境とRSの関係は必ずしも敵対的ではなく，協調・共生を前提とすることも多い．本研究では仕様の実現可能性必要条件に基づき協調的RSを自動合成する手法の開発を目的とし，関連研究の調査を行い，また，研究中に見出した実現可能 性必要条件群及び既知の実現可能性必要条件群の厳密な形式的定義を呼び階層定理群を与えた．
これらの実現可能性必要条件群は網羅性，保存可能性，安定化可能性及び戦略化可能性の4つの観点から体系的・階層的に分類でき，その観点から協力が発生し得ることを導くことができる．例えば，安定化可能性（相手からの一時的な協力により恒久的な安定状態へ到達し仕様を満たすことができるという性質）の観点からは，RS及び環境のそれぞれの目的（仕様）がそれぞれの立場から安定化可能であり，かつ，それぞれの安定状態へ到達するまでのお互い のふるまいが矛盾しないのであれば，RSを環境が協調することでそれぞれの目的（仕様）を満足することが可能となることが導出できる．また，保存可能性（仕様の充足可能性を保持し続けることができるという性質）の観点からも，類似の強調が発生する可能性を導出できる．ただし，必然的あるいは妥協的な協調強調が発生するための必要充分な条件を見出すには至っていない．
2020年度は，実現可能性必要条件群の特性について，判定手続きを構成するサブルーチンの共通性及び類似性からも分析し，また，各実現可能性必要条件判定の計算量を導出した．2021年度は，必然的あるいは妥協的な協調強調が発生するための必要充分な条件の確率に向けて，時間的性質の分類・特徴づけを再考し，新たな実現可能性必要条件は見出した．
|
| 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)
