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