| 研究課題/領域番号 |
19K11821
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 信州大学 |
|---|
研究代表者 |
和崎 克己 信州大学, 学術研究院工学系, 教授 (70271492)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2023-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円)
2022年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2021年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2020年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2019年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
|
|---|
| キーワード | 非同期並列システム / ハードウェアコンパイラ / 定理証明器 / モデル検査器 / 形式検証系 / 関数型言語系 / 状態空間生成 / ペトリネット / 形式検証 / モデル検査 |
|---|
| 研究開始時の研究の概要 |
定理証明のプロパティ検証情報とモデル検査時の空間最適分割問題を融合し，メニーコア・クラスタ基盤上へ実装する．システム統合のため，状態空間の最適分割・合成を行うためのアルゴリズム開発と並列化ライブラリを利用したプログラム開発を行う．非同期回路や並行システムに関する形式化記述として，Mizar Mathematical Library (MML) を利用する．並列化検証システム全体の性能評価と，実システムレベルでの性能評価のために，intel Xeon Phi並列アクセラレータと，FPGA/CPLD統合設計開発ツールを使用する．
|
| 研究成果の概要 |
検証対象とする回路の厳密プロパティ検査を目的とし、論理ゲート素子間の接続をメッセージパッシング型並列計算でモデル化する研究を実施した。定理証明は回路構造と接続の正当性に関するプロパティ検査を行った。スケーラブルでかつ繰り返し構造を有するPEの実例として、高速乗算回路の高基数コンプレッサモジュールについて実際に多ソート代数を理論的基盤とする定理証明を記述し、Mizarプルーフチェッカを用いた機械検証を行ったところ、回路合成の構造上の正しさならびに入出力関係の正しさなど所望のプロパティ検証に成功した。
|
| 研究成果の学術的意義や社会的意義 |
LOTOSコード生成器によって下位設計（ペトリネットモデル）が得られ、状態空間生成器を用いて初期状態から駆動するが、状態空間生成時の既生成マーキングを記憶するハッシュメモリの効率化を図るため、削除可能状態のオンライン判定アルゴリズムに関する検討を行った点に学術的意義がある。なおペトリネット検証系に関する基礎研究として、サブマーキング法を用いた状態空間の抽象化と準ホーム状態の存在検知、一般ペトリネットのSATソルバーを用いた構造解析による強L3活性構造の検知などに関する成果を得た点についても学術的意義がある。
|
