| 研究課題/領域番号 |
07J02056
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 国内 |
|---|
| 研究分野 |
電子デバイス・電子機器
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
西原 佑 東京大学, 大学院・工学系研究科, 特別研究員(DC1)
|
|---|
| 研究期間 (年度) |
2007 – 2009
|
| 研究課題ステータス |
完了 (2009年度)
|
| 配分額 *注記 |
2,700千円 (直接経費: 2,700千円)
2009年度: 900千円 (直接経費: 900千円)
2008年度: 900千円 (直接経費: 900千円)
2007年度: 900千円 (直接経費: 900千円)
|
|---|
| キーワード | 形式的検証 / モデル検査 / 割り込み / 有界モデル検査 / SMTソルバ / 順序化 / 並列モデル / 状態探索 / 等価性検証 / 限定モデル検査 / プロパティ分割 / ルールベース検 / FSMD / 高位合成 / HW / SW協調設計 / 項書き換えシステム / システム依存グラフ / ワードレベル |
|---|
| 研究概要 |
1.多段プロパティ分割とその改良を用いた有界モデル検査手法の三段階以上への拡張
前年度までに提案した有界モデル検査では二段階までの分割しか行えないため、初期状態から遠い位置に誤りがあった場合の検出が非効率的になるという問題があった、そこで、今年度は三段階以上の任意の分割が可能となるような手法の提案を行った。そのような分割方法では、各段階において異なるパラメータを使用できるため自由度が高い。そこで、効率的な探索が可能となるようなアルゴリズムを提案し、実験によりその効率性を確認した。また、手法全体に対してもよりフォーマルに再定義を行った。その結果、前年度よりも更に手法が詳細化・具体化され、手法の正当性が更に高まった。
2.割り込み処理の具体的なモデル化
まず、前年度までに扱えなかった割り込み処理について、並列モデルによってモデル化する手法を提案した。しかしながら、割り込みをモデル化した場合にはモデル全体の並列度が上昇し、検証の難易度が大幅に上昇する。そこで、並列モデルを逐次モデルに変換する技術である順序化を導入し検証の効率化を図った。既存の順序化手法では割り込みが扱えないためそれを割り込みを扱えるように拡張し、さらにSatisfiability Modulo Theory (SMT)ソルバを導入して考えられる全ての逐次記述を同時に出力できる手法を提案した。実験により、並列モデルの探索効率化手法である半順序簡約を用いた場合に比べて数倍の効率化を実現できていることが確認された。
|
