Fusion of Meta-Scalable Theorem Prover and Parallel Model Checker to Realize Large-Scale Fast Formal Verification
| Project/Area Number |
19K11821
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Shinshu University |
|---|
Principal Investigator |
Wasaki Katsumi 信州大学, 学術研究院工学系, 教授 (70271492)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2022: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2021: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2020: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2019: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | 非同期並列システム / ハードウェアコンパイラ / 定理証明器 / モデル検査器 / 形式検証系 / 関数型言語系 / 状態空間生成 / ペトリネット / 形式検証 / モデル検査 |
|---|
| Outline of Research at the Start |
定理証明のプロパティ検証情報とモデル検査時の空間最適分割問題を融合し，メニーコア・クラスタ基盤上へ実装する．システム統合のため，状態空間の最適分割・合成を行うためのアルゴリズム開発と並列化ライブラリを利用したプログラム開発を行う．非同期回路や並行システムに関する形式化記述として，Mizar Mathematical Library (MML) を利用する．並列化検証システム全体の性能評価と，実システムレベルでの性能評価のために，intel Xeon Phi並列アクセラレータと，FPGA/CPLD統合設計開発ツールを使用する．
|
| Outline of Final Research Achievements |
For the purpose of rigorous property checking of circuits to be verified, a study was conducted to model the connections between logic gate elements using message-passing parallel computation. Theorem proving was done by property checking on the circuit structure and the validity of the connections. As an actual example of PE with scalable and repetitive structures, we actually wrote a theorem proof for a high radix compressor module of a high-speed multiplier circuit using multisort algebra as the theoretical basis, and performed machine verification using the Mizar proof checker. The desired properties, such as the correctness of the circuit synthesis structure and input-output relations, were successfully verified.
|
| Academic Significance and Societal Importance of the Research Achievements |
LOTOSコード生成器によって下位設計（ペトリネットモデル）が得られ、状態空間生成器を用いて初期状態から駆動するが、状態空間生成時の既生成マーキングを記憶するハッシュメモリの効率化を図るため、削除可能状態のオンライン判定アルゴリズムに関する検討を行った点に学術的意義がある。なおペトリネット検証系に関する基礎研究として、サブマーキング法を用いた状態空間の抽象化と準ホーム状態の存在検知、一般ペトリネットのSATソルバーを用いた構造解析による強L3活性構造の検知などに関する成果を得た点についても学術的意義がある。
|
Report
(5 results)
Research Products
(26 results)
