2007 Fiscal Year Annual Research Report
述語抽象化検証による大規模組込みシステム向きオブジェクト指向設計自動検証手法
| Project/Area Number |
19500025
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
山根 智 Kanazawa University, 金沢大学・自然科学研究科, 教授 (70263506)
|
|---|
| Keywords | 組込みシステム / オブジェクト指向 / 述語抽象化洗練 |
|---|
| Research Abstract |
本年度は、以下の基礎理論を構築した。
(1)オブジェクト指向手法の中で、ステートチャートの検証は極めて重要である。本研究で、ステートチャートの検証において、並列と階層の状態を述語抽象化して、検証コスを削減する理論を構築した。さらに、偽反例かどうかを判定する手法を構築して、述語の洗練手法を構築した。以上により、ステートチャートの述語抽象化連戦検証理論を構築して、実証実験により、その有効性を実証した。
(2)リアルタイム性の検証も重要である。本研究で、タイミング制約を表現する述語を用いて、述語抽象化して、検証コスを削減する理論を構築した。さらに、偽反例かどうかを判定する手法を構築して、述語の洗練手法を構築した。以上により、リアルタイムシステムの述語抽象化連戦検証理論を構築して、実証実験により、その有効性を実証した。
今後は、以上の(1)と(2)とを融合して、組込みシステム向きのオブジェクト指向仕様の述語抽象化洗練検証手法を構築する予定である。
|
