A divide and conquer approach to parallelization of LTL model checking
| Project/Area Number |
19H04082
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
OGATA Kazuhiro 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥16,770,000 (Direct Cost: ¥12,900,000、Indirect Cost: ¥3,870,000)
Fiscal Year 2022: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2021: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2020: ¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2019: ¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
|
|---|
| Keywords | モデル検査 / 分割統治 / 並列化 / leads-to性 / eventual性 / 条件付安定性 / until性 / until安定性 / 状態空間爆発 / 線形時相論理 / Maude / 状態爆発 / LTL / Leads-to性質 / 状態機械 |
|---|
| Outline of Research at the Start |
我々の生活を便利にするシステムは高信頼であるべきだ。さもなければ、多額の財産を失う等の多大な不便をこうむることになる。システムを高信頼にするために使うことのできる技術のひとつはモデル検査である。システムが期待される要件を満たすかどうかを自動で検証出来る。しかし、システムの到達可能状態空間が大きくなり過ぎてモデル検査不能になる問題が起こる。本研究計画では、到達可能状態空間を複数の部分空間に分割し、各々の部分空間でモデル検査を行えるようにすることでこの問題を緩和することを試みる。加えて、複数の部分空間に対するモデル検査を同時並列に実行することでモデル検査の効率化も試みる。
|
| Outline of Final Research Achievements |
By splitting an infinite state tree constructed from each initial state into multiple layers and tackling each sub-state space, the state space explosion in model checking can be alleviated. By handling multiple sub-state spaces simultaneously, the model checking running performance can be improved. Several important classes of linear temporal logic (LTL) properties, such as leads-to properties, can be dealt with. We built sequential and parallel versions of a support tool for each property class and conduct cases studies with such tools, demonstrating the usefulness of the techniques proposed and the support tools.
|
| Academic Significance and Societal Importance of the Research Achievements |
ソフトウェアは我々の生活に深く入り込んでいる。大変便利であるが、複雑であればあるほど潜在的不具合が存在する可能性は大きい。顕在化すると、財政的損失ばかりでなく人命にも危険が及ぶ可能性すらある。このため、潜在的不具合は可能な限り取り除いたほうが良い。そのための有望な技術にモデル検査がある。しかし、ソフトウェア産業界において日常業務での使用に耐えうるようにするには解決すべき課題がある。状態空間爆発の緩和と実行速度の改善だ。状態空間を複数の空間に分割することで状態空間爆発を緩和し、複数の部分状態空間を並列にモデル検査することで実行速度を改善した。ソフトウェア産業界での実用化に向けて前進できた。
|
Report
(5 results)
Research Products
(27 results)
