| 研究課題/領域番号 |
19H04082
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
緒方 和博 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2023-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
16,770千円 (直接経費: 12,900千円、間接経費: 3,870千円)
2022年度: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
2021年度: 4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2020年度: 4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円)
2019年度: 4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円)
|
|---|
| キーワード | モデル検査 / 分割統治 / 並列化 / leads-to性 / eventual性 / 条件付安定性 / until性 / until安定性 / 状態空間爆発 / 線形時相論理 / Maude / 状態爆発 / LTL / Leads-to性質 / 状態機械 |
|---|
| 研究開始時の研究の概要 |
我々の生活を便利にするシステムは高信頼であるべきだ。さもなければ、多額の財産を失う等の多大な不便をこうむることになる。システムを高信頼にするために使うことのできる技術のひとつはモデル検査である。システムが期待される要件を満たすかどうかを自動で検証出来る。しかし、システムの到達可能状態空間が大きくなり過ぎてモデル検査不能になる問題が起こる。本研究計画では、到達可能状態空間を複数の部分空間に分割し、各々の部分空間でモデル検査を行えるようにすることでこの問題を緩和することを試みる。加えて、複数の部分空間に対するモデル検査を同時並列に実行することでモデル検査の効率化も試みる。
|
| 研究成果の概要 |
各々の初期状態から作成される無限状態木を複数の層に分割し、複数の部分状態空間を生成し、各々の部分状態を個別にモデル検査することで、モデル検査における状態空間爆発問題を緩和した。複数の部分状態空間を並列にモデル検査することで、モデル検査の実行性能を改善した。leads-to性などの線形時相論理で記述可能な重要な性質のいくつかのクラスを扱うことができる。各々の性質のクラスごとに、逐次版と並列版の支援ツールを開発した。それらの支援ツールを用いた事例研究により提案技術と支援ツールの有効性を確認した。
|
| 研究成果の学術的意義や社会的意義 |
ソフトウェアは我々の生活に深く入り込んでいる。大変便利であるが、複雑であればあるほど潜在的不具合が存在する可能性は大きい。顕在化すると、財政的損失ばかりでなく人命にも危険が及ぶ可能性すらある。このため、潜在的不具合は可能な限り取り除いたほうが良い。そのための有望な技術にモデル検査がある。しかし、ソフトウェア産業界において日常業務での使用に耐えうるようにするには解決すべき課題がある。状態空間爆発の緩和と実行速度の改善だ。状態空間を複数の空間に分割することで状態空間爆発を緩和し、複数の部分状態空間を並列にモデル検査することで実行速度を改善した。ソフトウェア産業界での実用化に向けて前進できた。
|
