2022 Fiscal Year Annual Research Report
Fusion of Meta-Scalable Theorem Prover and Parallel Model Checker to Realize Large-Scale Fast Formal Verification
| Project/Area Number |
19K11821
|
|---|
| Research Institution | Shinshu University |
|---|
Principal Investigator |
和崎 克己 信州大学, 学術研究院工学系, 教授 (70271492)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | 非同期並列システム / ハードウェアコンパイラ / 定理証明器 / モデル検査器 / 形式検証系 / 関数型言語系 / 状態空間生成 / ペトリネット |
|---|
| Outline of Annual Research Achievements |
(1) 検証対象とする回路の厳密プロパティ検査を目的とし、論理ゲート素子間の接続をメッセージパッシング型並列計算でモデル化する研究を実施した。定理証明は回路構造と接続の正当性に関するプロパティ検査を行った。スケーラブルでかつ繰り返し構造を有するPEの実例として、高速乗算回路の高基数コンプレッサモジュールについて実際に多ソート代数を理論的基盤とする定理証明を記述し、Mizarプルーフチェッカを用いた機械検証を行ったところ、回路合成の構造上の正しさならびに入出力関係の正しさなど所望のプロパティ検証に成功した。
(2) LOTOSコード生成器によって下位設計（ペトリネットモデル）が得られ、状態空間生成器を用いて初期状態から駆動するが、状態空間生成時の既生成マーキングを記憶するハッシュメモリの効率化を図るため、削除可能状態のオンライン判定アルゴリズムに関する検討を行った。なおペトリネット検証系に関する基礎研究として、サブマーキング法を用いた状態空間の抽象化と準ホーム状態の存在検知、一般ペトリネットのSATソルバーを用いた構造解析による強L3活性構造の検知などに関する成果を得た。
(3) 上位設計としての対象回路の構成情報は、簡易な回路記述に文法を縮約した関数型プログラミング言語系の上で記述するが、LOTOSコード生成器は既にフランス INRIA/VASYからCADPツールの提供とライセンスを受けており、モデル検査が実際に実行できるまでの環境の構築は終わっており、この課題に関する研究は順著に進捗している。CADPツール側では特にイタレーション・モデルの記述に適したLOTOS-NT(LNT)拡張言語へのサポートは可能な状態であるので、今後は、成果物であるDILLライブラリのLNT化など、今後の進捗が待たれている。
|
| Remarks |
HiPS tool is developed at the Department of Computer Science and Engineering, Shinshu University, which is a tool design and analysis of Petri nets, developed using Microsoft Visual C # and C++.
|
