振る舞い仕様の効率的な実現可能性判定のための分割検証法
| Project/Area Number |
22K11980
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Takushoku University |
|---|
Principal Investigator |
島川 昌也 拓殖大学, 工学部, 准教授 (00749161)
|
|---|
| Project Period (FY) |
2022-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
Fiscal Year 2024: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2023: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2022: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Keywords | 仕様検証 / 実現可能性 / ω-オートマトン |
|---|
| Outline of Research at the Start |
時間論理などでシステムの振る舞いに関する仕様を厳密に記述し，それを検証する形式仕様検証は，人力では見つけにくい欠陥を計算機によって自動で検出できるが，計算コストが高いという問題がある．中でも実現可能性と呼ばれる性質の判定のコストは特に高く，それが実用上の障壁となっている．
本研究では，実現可能性判定を効率的に行う分割検証法について検討する．分割検証法では，仕様をいくつかのサブモジュールに分割し，各サブモジュールで部分検証を行ったのち，その結果を統合して仕様全体の検証を行う．各サブモジュールの部分検証のフェーズで余分な情報を除去できるため，一括検証に比べて効率的な検証が期待できる．
|
| Outline of Annual Research Achievements |
時間論理などでシステムの振る舞いに関する仕様を厳密に記述し，それを検証する形式仕様検証は，人力では見つけにくい欠陥を計算機によって自動で検出できるが，計算コストが高いという問題がある．本研究では，特に計算コストが高いリアクティブシステム仕様の実現可能性判定の効率化を目的として，分割検証法について検討する．
ここで検討する分割検証の枠組みは次のとおりである：(1)仕様をいくつかのサブモジュールに分割，(2)各サブモジュール仕様について，それと等価なωオートマトンを構成，(3)各サブモジュール仕様のオートマトンに簡約などを適用，(4)各サブモジュール仕様のオートマトンを統合，(5)統合したオートマトンを分析．このような分割検証では，ステップ3の簡約方法が全体としての効率を大きく左右する．本研究では，そこへ新たなアイディアを導入する．既存研究では，単なるオートマトンの最小化（等価な変換）しか行われていなかったが，本研究では，統合後の検証で不必要な局所的な情報の除去（意味的にも異なる変換）も行う．
2022年度は，サブモジュール仕様のオートマトンの簡約において，局所的な「応答イベント」の情報を除去する分割検証を提案した（リアクティブシステム仕様は要求イベントと応答イベントの生起タイミングを規定するものである）．そして，その正当性，つまり，提案した方法では局所的な応答イベント情報の除去を行っても正しく実現可能性の判定が行えること（除去しないときと同様の判定結果が得られること）を証明した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
新たな分割検証法の検討を行い，一定の成果が得られた．それゆえ，現在までの進捗状況はおおむね順調であると判断した．
|
| Strategy for Future Research Activity |
今年度提案した分割検証法を実装する．そして，その効率を実験により確認する．
|
Report
(1 results)
Research Products
(1 results)
