| 研究課題/領域番号 |
24500034
|
|---|
| 研究機関 | 金沢大学 |
|---|
研究代表者 |
山根 智 金沢大学, 電子情報学系, 教授 (70263506)
|
|---|
| キーワード | 動的再構成可能組込みシステム / 動的ハイブリッドオートマトン / CEGAR / 仕様記述 / モデル検査 / 検証器 |
|---|
| 研究概要 |
前年度，動的再構成可能組込みシステムの仕様記述言語である動的ハイブリッドオートマトンの構文と意味の開発，仕様記述例の開発及び検証手法の開発は順調に進んだ．本年度は前年度の成果をもとに，以下を行った．
(1)開発した仕様記述例を改良して，並列オブジェクト指向により，動的再構成可能組込みシステムを仕様記述できることが確認できた．
(2)抽象化と精錬によるモデル検査手法である動的ハイブリッドCEGAR(CounterExample Guided Abstraction and Refinement)検証器をほぼ実装し終えた．同時に，動的ハイブリッドオートマトン及び動的ハイブリッドCEGARの効果を評価するために，通常のハイブリッドオートマトンのモデル検査器を実装した．
今後は動的ハイブリッドCEGAR検証器を完成させて，その有効性を実問題で評価する．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
動的ハイブリッドCEGAR(CounterExample Guided Abstraction and Refinement)検証器の実装に関して，試験を完全には終えていない．
しかし，間もなく完全に正常動作を確認できる見込みである．
|
| 今後の研究の推進方策 |
今後は動的ハイブリッドCEGAR検証器を完成させて，その有効性を実問題で評価する．
また，検証器の実装を改良する．
さらに，SMT等の最新のソフトウェアモデル検査理論を用いて検証器の方式を改良する．
|
