2016 Fiscal Year Research-status Report
非近似的アプローチによるリアクティブシステム仕様の効率的な実現可能性判定法
| Project/Area Number |
15K15969
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
島川 昌也 東京工業大学, 情報理工学院, 助教 (00749161)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | リアクティブシステム仕様 / 実現可能性 / ω-オートマトン |
|---|
| Outline of Annual Research Achievements |
リアクティブシステム仕様の実現可能性に関する検証は，仕様記述において見過ごされがちな危険な状況に陥る可能性を検出することができるが，一般に煩雑で計算コストの高い処理を伴う．本研究ではリアクティブシステム仕様の実現可能性検証の効率化を目的とし，本年度は以下について取り組んだ．
＜on-the-fly簡約手法＞：リアクティブシステム仕様の実現可能性検証においては，仕様から決定性ωオートマトンを構成する必要がある．近似を行わない場合，その手続は煩雑でコストが高い．模倣関係や強連結成分情報を利用し，ωオートマトンを簡約する手法について多く研究されている．それらの多くは，構成後のオートマトンに対して適用されるものである．本研究では，構成途中に簡約を適用することで扱う状態やエッジを減らし，構成自体のコストも低減させるon-the-fly簡約について検討する．本年度は，決定性ωオートマトン構成時に状態にラベルされる情報を利用して簡約を行う手法の開発を進めた．
＜分割検証法＞：分割検証とは，次のようなものである．i)分割されたそれぞれの部分仕様において決定性ωオートマトンを構成する．ii)各部分オートマトンにおいて局所的な情報を捨象する．iii)各部分オートマトンを統合し，解析する．このような検証では，ii)において局所的な情報を捨象できるため，一括検証に比べて高速に判定を行える．本年度においては，効率的な分割検証を行うための仕様の分割方法を提案した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
on-the-fly簡約手法や分割検証法について検討し，一定の成果が得られた．それゆえ，現在までの進捗状況はおおむね順調であると判断した．
|
| Strategy for Future Research Activity |
これまでに提案してきた効率化手法を織り込んだ実現可能性判定器の実装を行う予定である．また，これまでの研究成果を整理し，様々な形で公表していく予定である．
|
| Causes of Carryover |
国際会議・国内学会の参加費・旅費，及び英文校正費用にあてる予定であった分が学内予算でまかなえたため，次年度使用額が生じた．
|
| Expenditure Plan for Carryover Budget |
開発・実験を行う上で必要となるPC周辺機器を購入する予定である．残りは当初の計画通り，国際会議・国内学会の参加費・旅費，及び英文校正費用等にあてる予定である．
|
