2013 Fiscal Year Research-status Report
動的ハイブリッドオートマトンによる動的再構成可能組込みシステムの高度な設計検証
| Project/Area Number |
24500034
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
山根 智 金沢大学, 電子情報学系, 教授 (70263506)
|
|---|
| Keywords | 動的再構成可能組込みシステム / 動的ハイブリッドオートマトン / CEGAR / 仕様記述 / モデル検査 / 検証器 |
|---|
| Research Abstract |
前年度，動的再構成可能組込みシステムの仕様記述言語である動的ハイブリッドオートマトンの構文と意味の開発，仕様記述例の開発及び検証手法の開発は順調に進んだ．本年度は前年度の成果をもとに，以下を行った．
(1)開発した仕様記述例を改良して，並列オブジェクト指向により，動的再構成可能組込みシステムを仕様記述できることが確認できた．
(2)抽象化と精錬によるモデル検査手法である動的ハイブリッドCEGAR(CounterExample Guided Abstraction and Refinement)検証器をほぼ実装し終えた．同時に，動的ハイブリッドオートマトン及び動的ハイブリッドCEGARの効果を評価するために，通常のハイブリッドオートマトンのモデル検査器を実装した．
今後は動的ハイブリッドCEGAR検証器を完成させて，その有効性を実問題で評価する．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
動的ハイブリッドCEGAR(CounterExample Guided Abstraction and Refinement)検証器の実装に関して，試験を完全には終えていない．
しかし，間もなく完全に正常動作を確認できる見込みである．
|
| Strategy for Future Research Activity |
今後は動的ハイブリッドCEGAR検証器を完成させて，その有効性を実問題で評価する．
また，検証器の実装を改良する．
さらに，SMT等の最新のソフトウェアモデル検査理論を用いて検証器の方式を改良する．
|
