ハードウェア/ソフトウェア協調設計に対する形式的検証とその要素技術に関する研究

1.多段プロパティ分割とその改良を用いた有界モデル検査手法の三段階以上への拡張前年度までに提案した有界モデル検査では二段階までの分割しか行えないため、初期状態から遠い位置に誤りがあった場合の検出が非効率的になるという問題があった、そこで、今年度は三段階以上の任意の分割が可能となるような手法の提案を行った。そのような分割方法では、各段階において異なるパラメータを使用できるため自由度が高い。そこで、効率的な探索が可能となるようなアルゴリズムを提案し、実験によりその効率性を確認した。また、手法全体に対してもよりフォーマルに再定義を行った。その結果、前年度よりも更に手法が詳細化・具体化され、手法の正当性が更に高まった。2.割り込み処理の具体的なモデル化まず、前年度までに扱えなかった割り込み処理について、並列モデルによってモデル化する手法を提案した。しかしながら、割り込みをモデル化した場合にはモデル全体の並列度が上昇し、検証の難易度が大幅に上昇する。そこで、並列モデルを逐次モデルに変換する技術である順序化を導入し検証の効率化を図った。既存の順序化手法では割り込みが扱えないためそれを割り込みを扱えるように拡張し、さらにSatisfiability Modulo Theory (SMT)ソルバを導入して考えられる全ての逐次記述を同時に出力できる手法を提案した。実験により、並列モデルの探索効率化手法である半順序簡約を用いた場合に比べて数倍の効率化を実現できていることが確認された。

1.多段プロパティ分割とその改良を用いた有界モデル検査手法の三段階以上への拡張前年度までに提案した有界モデル検査では二段階までの分割しか行えないため、初期状態から遠い位置に誤りがあった場合の検出が非効率的になるという問題があった、そこで、今年度は三段階以上の任意の分割が可能となるような手法の提案を行った。そのような分割方法では、各段階において異なるパラメータを使用できるため自由度が高い。そこで、効率的な探索が可能となるようなアルゴリズムを提案し、実験によりその効率性を確認した。また、手法全体に対してもよりフォーマルに再定義を行った。その結果、前年度よりも更に手法が詳細化・具体化され、手法の正当性が更に高まった。2.割り込み処理の具体的なモデル化まず、前年度までに扱えなかった割り込み処理について、並列モデルによってモデル化する手法を提案した。しかしながら、割り込みをモデル化した場合にはモデル全体の並列度が上昇し、検証の難易度が大幅に上昇する。そこで、並列モデルを逐次モデルに変換する技術である順序化を導入し検証の効率化を図った。既存の順序化手法では割り込みが扱えないためそれを割り込みを扱えるように拡張し、さらにSatisfiability Modulo Theory (SMT)ソルバを導入して考えられる全ての逐次記述を同時に出力できる手法を提案した。実験により、並列モデルの探索効率化手法である半順序簡約を用いた場合に比べて数倍の効率化を実現できていることが確認された。