| 研究課題/領域番号 |
18K18028
|
|---|
| 研究機関 | 拓殖大学 |
|---|
研究代表者 |
島川 昌也 拓殖大学, 工学部, 助教 (00749161)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2023-03-31
|
| キーワード | ωオートマトン / 仕様検証 |
|---|
| 研究実績の概要 |
時間論理などの数学的な言語でシステムの振る舞い(トレース)についての仕様を厳密に記述し，それを検証する形式仕様検証は，人力では見つけにくい欠陥を計算機によって自動で検出できるが，計算コストが高いという問題がある．本研究では，時間論理仕様の検証の効率化に向けて，仕様検証において基礎となるωオートマトンや無限ゲームの操作・判定の効率化手法の提案，及びそれを利用した効率的な仕様検証器の実装を行う.
2021年度は，これまでに引き続き，部分シンボリック技法による効率的な実装手法の開発に取り組んだ．通常のシンボリック技法では，オートマトン全体をひとつのBinary Decision Diagram (BDD)で表現するのに対して，部分シンボリック技法ではBDDを部分的に利用する．通常のシンボリック技法には，煩雑な手続きへの適用が難しいという問題がある一方，部分シンボリック技法は，適用可能な範囲が広いという特徴を持つ．本年度は，部分シンボリック技法には複数のバリエーションがあるため，それらについて検討を行った．具体的には，次の2種類の部分シンボリックについて検討した：(i) 各遷移にラベルされる遷移条件をひとつのBDDで表現するアプローチ，(ii) 各状態からの複数の遷移をひとつのBDDで表現するアプローチ（BDDの変種であるMtBDDを利用）．また，この2種類の部分シンボリック技法のユニバーサルω木オートマトンの空判定への適用についても検討し，実際にそのパフォーマンスを実験により確認した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
仕様検証において基礎となるωオートマトン操作・判定の効率的な実装手法の開発に取り組み，一定の成果が得られた．それゆえ，現在までの進捗状況はおおむね順調であると判断した．
|
| 今後の研究の推進方策 |
これまでに検討した部分シンボリック技法を，ユニバーサルω木オートマトンの空判定以外の判定に適用することについて検討し，実験によりそのパフォーマンスを確認する予定である．
|
| 次年度使用額が生じた理由 |
(理由) 新型コロナウイルス感染症の影響で，国際会議に参加することができなかったため，次年度使用額が生じた．
(利用計画) 実験のための計算機の新調を検討している．
|
