2021 Fiscal Year Research-status 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 |
検証対象とする回路の厳密プロパティ検査を目的とし，論理ゲート素子間の接続をメッセージパッシング型並列計算でモデル化する研究を継続している．定理証明は回路構造と接続の正当性に関するプロパティ検査に専念する．実規模での組合せ回路全体での振る舞い検証は，並列化モデルチェッカを用いて検証することになるが，スケーラブルでかつ繰り返し構造を有するPEの実例として，高速乗算回路の高基数コンプレッサモジュールについて実際に多ソート代数を理論的基盤とする定理証明を記述し，Mizarプルーフチェッカを用いた機械検証を行ったところ，回路合成の構造上の正しさならびに入出力関係の正しさなど所望のプロパティ検証に既に成功している．
現在，関数型言語系の上のハードウェアコンパイラを機能拡張する目的のため，開発中の Melasy+ ハードウェアコンパイラについて，各演算機能に相当するLOTOSライブラリを機能拡張する研究を実施している．具体的には，高位設計としての対象回路の構成情報として，観測レベル，振る舞いレベル，ゲートレベルの3種のライブラリとしてレベル別設計を行い，各々のレベル間での相互検証を可能とした．
更に，LOTOSコード生成器によって下位設計（ペトリネットモデル）が得られ，状態空間生成器を用いて初期状態から駆動するが，状態空間生成時の既生成マーキングを記憶するハッシュメモリの効率化を図るため，削除可能状態のオンライン判定アルゴリズムに関する検討を行った．なおペトリネット検証系に関する基礎研究として，サブマーキング法を用いた状態空間の抽象化と準ホーム状態の存在検知，一般ペトリネットのSATソルバーを用いた構造解析による強L3活性構造の検知などに関する成果を得た．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
関数型言語系の上のハードウェアコンパイラを機能拡張する目的のため，開発中の Melasy+ ハードウェアコンパイラについて，各演算機能に相当するLOTOSライブラリを拡張する実装を行い，この課題に関する成果を発表済である(ITNG2022)．また，LOTOSコード生成器によって下位設計（ペトリネットモデル）が得られ，状態空間生成器を用いて初期状態から駆動するが，状態空間生成時の既生成マーキングを記憶するハッシュメモリの効率化（削除可能状態のオンライン判定アルゴリズム）に関する実装を行い，この課題に関する成果も発表済である(ITNG2022)．ただし，LOTOSコード生成器の実装と機能については中途の状態で，今後の進捗が待たれている．
上位設計としての対象回路の構成情報は，簡易な回路記述に文法を縮約した関数型プログラミング言語系の上で記述するが，LOTOSコード生成器は既にフランス INRIA/VASYからCADPツールの提供とライセンスを受けており，モデル検査が実際に実行できるまでの環境の構築は終わっており，この課題に関する研究は順著に進捗している．CADPツール側では特にイタレーション・モデルの記述に適したLOTOS-NT(LNT)拡張言語へのサポートは可能な状態であるので，今後は，成果物であるDILLライブラリのLNT化など，今後の進捗が待たれている．
|
| Strategy for Future Research Activity |
申請書の内容に基づき，プルーフチェッカとモデル検査器を並列化，メニーコア・クラスタ基盤へ実装する準備を進める．これは正当性（プロパティ）検証済の回路ライブラリを基礎とし，プルーフチェッカとモデル検査器を並列化し，メニーコア・クラスタ基盤へ実装するものである．システム統合のため，証明の分割・合成を行うためのシステム構築ならびにintel TBB並列化ライブラリを利用したプログラム開発を行う．具体的には，多数のPE群の動作検証のため，振る舞い状態空間を最適分割することで，メニーコアプロセッサ上での高スケーラブルな検証を，実サイズレベルまで強化する．構成されたクラスタ基盤上に，Mizarプルーフチェッカ・定理証明エンジンと，モデル検査器の実行プログラムを並列化コンパイラを用いて実装を進めていく.
ここまでの研究が順調に進捗した前提で，令和4年度は，並列化ライブラリを利用した総合的なプログラム開発に着手する．ここでは形式検証統合システムの並列化部分の性能向上を行う．具体的には，システム統合のため，状態空間の分割・合成を行うためのアルゴリズム開発と，並列化ライブラリを利用した総合的なプログラム開発を行う．性能評価対象は，パイプラインあるいはトーラス接続された超並列演算器（PE）とする．計算を多ソート代数でモデル化し，超並列接続のための制御器のモデルによって多数のPEをネットワーク・オートマタによって論理接続した構成とする．
|
| Causes of Carryover |
新型コロナウイルス感染症の影響により，2021年4月・9月に予定されていた国際・国内会議（ITNG, 情報処理学会FIT）がオンライン開催となり，出張等旅費が執行されなくなったため，次年度使用額がプラスとなった．
令和4年度の新型コロナウイルス感染症の影響は未だ見通せない状況ではあるが，対外発表の機会を捉えつつ，今回発生した次年度使用額は有効に執行を計画していきたい．
|
Research Products
(8 results)
