| 研究課題/領域番号 |
22K11980
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 拓殖大学 |
|---|
研究代表者 |
島川 昌也 拓殖大学, 工学部, 准教授 (00749161)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
3,250千円 (直接経費: 2,500千円、間接経費: 750千円)
2024年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2023年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2022年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 仕様検証 / 実現可能性 / ω-オートマトン |
|---|
| 研究開始時の研究の概要 |
時間論理などでシステムの振る舞いに関する仕様を厳密に記述し，それを検証する形式仕様検証は，人力では見つけにくい欠陥を計算機によって自動で検出できるが，計算コストが高いという問題がある．中でも実現可能性と呼ばれる性質の判定のコストは特に高く，それが実用上の障壁となっている．
本研究では，実現可能性判定を効率的に行う分割検証法について検討する．分割検証法では，仕様をいくつかのサブモジュールに分割し，各サブモジュールで部分検証を行ったのち，その結果を統合して仕様全体の検証を行う．各サブモジュールの部分検証のフェーズで余分な情報を除去できるため，一括検証に比べて効率的な検証が期待できる．
|
| 研究実績の概要 |
時間論理などでシステムの振る舞いに関する仕様を厳密に記述し，それを検証する形式仕様検証は，人力では見つけにくい欠陥を計算機によって自動で検出できるが，計算コストが高いという問題がある．本研究では，計算コストが特に高いリアクティブシステム仕様の実現可能性判定の効率化を目的として，分割検証法について検討する．
本研究で検討する分割検証の枠組みは次のとおりである：(1)仕様をいくつかのサブモジュールに分割，(2)各サブモジュール仕様について，それと等価なωオートマトンを構成，(3)各サブモジュール仕様のオートマトンに簡約などを適用，(4)各サブモジュール仕様のオートマトンを統合・分析．
このような分割検証では，ステップ(3)の簡約方法が全体としての効率を大きく左右する．本研究では，そこへ新たなアイディアを導入する．既存研究では単なるオートマトンの縮小化しか行われていなかったが，本研究では統合後の検証で不必要な局所的な情報の除去も行う．2022年度に本研究ではサブモジュール仕様のオートマトンの簡約において，局所的な「応答イベント」の情報を除去する分割検証法を提案し，その正当性，つまりその手法で正しく実現可能性の判定が行えることを証明している．
2023年度は，2022年度に提案した分割検証法の実装を行い，実験によりその性能を確認した．既存の分割検証ツールAcacia+と判定時間を比較したところ，提案手法の性能が既存ツールを大きく上回ることがわかった．これはステップ(3)における局所イベント情報の除去が効いたためであると考える．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初の予定どおり昨年度に提案した検証手法の評価実験を実施し，提案手法の有効性が確認できた．それゆえ，現在までの進捗状況はおおむね順調であると判断した．
|
| 今後の研究の推進方策 |
本研究で対象する分割検証法は，仕様の分割方法によって，そのパフォーマンスは大きく変わる．そのため，効果的な仕様の分割方法を検討する予定である．
|
