|
本年度は、以下の基礎理論を構築した。
(1)オブジェクト指向手法の中で、ステートチャートの検証は極めて重要である。本研究で、ステートチャートの検証において、並列と階層の状態を述語抽象化して、検証コスを削減する理論を構築した。さらに、偽反例かどうかを判定する手法を構築して、述語の洗練手法を構築した。以上により、ステートチャートの述語抽象化連戦検証理論を構築して、実証実験により、その有効性を実証した。
(2)リアルタイム性の検証も重要である。本研究で、タイミング制約を表現する述語を用いて、述語抽象化して、検証コスを削減する理論を構築した。さらに、偽反例かどうかを判定する手法を構築して、述語の洗練手法を構築した。以上により、リアルタイムシステムの述語抽象化連戦検証理論を構築して、実証実験により、その有効性を実証した。
今後は、以上の(1)と(2)とを融合して、組込みシステム向きのオブジェクト指向仕様の述語抽象化洗練検証手法を構築する予定である。
|
