2017 Fiscal Year Research-status Report
非近似的アプローチによるリアクティブシステム仕様の効率的な実現可能性判定法
| Project/Area Number |
15K15969
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
島川 昌也 東京工業大学, 情報理工学院, 助教 (00749161)
|
|---|
| Project Period (FY) |
2015-04-01 – 2019-03-31
|
| Keywords | リアクティブシステム仕様 / 実現可能性 / ω-オートマトン |
|---|
| Outline of Annual Research Achievements |
リアクティブシステム仕様の実現可能性に関する検証は，仕様記述において見過ごされがちな危険な状況に陥る可能性を検出することができるが，一般に煩雑で計算コストの高い処理を伴う．本研究ではリアクティブシステム仕様の実現可能性検証の効率化を目的とし，本年度は以下について取り組んだ．
＜効率的な実現可能性判定器の実装＞：これまでに与えた効率的な決定性ωオートマトン構成法を基に実現可能性判定器の実装を進めた．また，平成27年度に与えた実現可能性のSATソルバーを用いる有界検査法のさらなる効率化にも取り組んだ．
＜実現可能性の必要条件判定＞：強充足可能性と呼ばれる実現可能性の必要条件の判定についても検討した．過去の研究で我々は，強充足可能性判定の計算量理論的コストが実現可能性のそれよりも低いことを明らかにしている．ここでは，実際的なコストについて調査した．具体的には，強充足可能性判定器を実装し，ベンチマークによって，強充足可能性が実現可能性よりも高速に判定できることを確認した．強充足可能性は実現可能性の必要条件であるため，その判定で仕様に欠陥がないことを保障することはできないが，ある種の欠陥を効率的に検出できることが確認できた．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
実現可能性判定器や強充足可能性（必要条件）判定器の実装を進め，一定の成果が得られた．それゆえ，現在までの進捗状況はおおむね順調であると判断した．
|
| Strategy for Future Research Activity |
これまでの研究成果を整理し，論文等で発表していく．また，研究全体の総括を行っていく予定である．
|
| Causes of Carryover |
＜次年度使用額が生じた理由＞：国際会議の参加費／旅費，及び英文校正費用の一部を学内予算でまかなえたため，次年度使用額が生じた．
＜使用計画＞：国際会議・国内学会の参加費／旅費，及び英文校正費等として使用する予定である．また，研究を行う上で必要となる消耗品等を購入する．
|
