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

软硬件协同设计形式化验证及其关键技术研究

基本信息

批准号：
07J02056
负责人：
西原佑
金额：
$ 1.73万
依托单位：
The University of Tokyo
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2007
资助国家：
日本
起止时间：
2007 至 2009
项目状态：
已结题

项目摘要

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

1.使用多阶段属性划分将有界模型检查方法扩展到三个或更多阶段及其改进由于前一年提出的有界模型检查只能执行最多两个阶段的划分，因此存在检测的问题。错误会导致效率低下，因此今年我们提出了一种允许任意划分为三个或更多阶段的方法。这种划分方法具有很高的自由度，因为每个阶段可以使用不同的参数。因此，我们提出了一种能够实现高效搜索的算法，并通过实验证实了其效率。我们还更正式地重新定义了整个方法。因此，该办法比上一年更加详细和具体，进一步增强了其合法性。 2.中断处理的具体建模首先，我们提出了一种使用并行模型对去年无法处理的中断处理进行建模的方法。然而，当对中断进行建模时，整个模型的并行度增加，这大大增加了验证的难度。因此，我们引入了排序这一将并行模型转换为顺序模型的技术，以提高验证效率。由于现有的排序方法无法处理中断，因此我们对其进行了扩展以处理中断，并提出了一种通过引入可满足性模理论（SMT）求解器来同时输出所有可能的顺序描述的方法。实验证实该方法比使用偏序约简的效率高数倍，是一种提高并行模型搜索效率的方法。