研究課題
(1) 検証対象とする回路の厳密プロパティ検査を目的とし、論理ゲート素子間の接続をメッセージパッシング型並列計算でモデル化する研究を実施した。定理証明は回路構造と接続の正当性に関するプロパティ検査を行った。スケーラブルでかつ繰り返し構造を有するPEの実例として、高速乗算回路の高基数コンプレッサモジュールについて実際に多ソート代数を理論的基盤とする定理証明を記述し、Mizarプルーフチェッカを用いた機械検証を行ったところ、回路合成の構造上の正しさならびに入出力関係の正しさなど所望のプロパティ検証に成功した。(2) LOTOSコード生成器によって下位設計（ペトリネットモデル）が得られ、状態空間生成器を用いて初期状態から駆動するが、状態空間生成時の既生成マーキングを記憶するハッシュメモリの効率化を図るため、削除可能状態のオンライン判定アルゴリズムに関する検討を行った。なおペトリネット検証系に関する基礎研究として、サブマーキング法を用いた状態空間の抽象化と準ホーム状態の存在検知、一般ペトリネットのSATソルバーを用いた構造解析による強L3活性構造の検知などに関する成果を得た。(3) 上位設計としての対象回路の構成情報は、簡易な回路記述に文法を縮約した関数型プログラミング言語系の上で記述するが、LOTOSコード生成器は既にフランス INRIA/VASYからCADPツールの提供とライセンスを受けており、モデル検査が実際に実行できるまでの環境の構築は終わっており、この課題に関する研究は順著に進捗している。CADPツール側では特にイタレーション・モデルの記述に適したLOTOS-NT(LNT)拡張言語へのサポートは可能な状態であるので、今後は、成果物であるDILLライブラリのLNT化など、今後の進捗が待たれている。
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++.
すべて 2023 2022 その他
すべて 雑誌論文 (4件) (うち査読あり 4件) 学会発表 (4件) 備考 (1件)
Proceedings of 20th International Conference on Information Technology-New Generations (ITNG 2023), Advances in Intelligent Systems and Computing, Springer
巻: 1459 ページ: -
Proceedings of 19th International Conference on Information Technology-New Generations (ITNG 2022), Advances in Intelligent Systems and Computing, Springer
巻: 1421 ページ: 387-392
10.1007/978-3-030-97652-1_46
巻: 1421 ページ: 393-398
10.1007/978-3-030-97652-1_47
Proceedings of the 15th Conference on Intelligent Computer Mathematics (CICM 2022), LNAI
巻: 13467 ページ: 141-146
10.1007/978-3-031-16681-5_9
https://github.com/kisolab/HiPS1_released
