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