2018 Fiscal Year Final Research Report
Liveness verification in software model checking
| Project/Area Number |
16K00109
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Tsurumi University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 光晴 千葉大学, 大学院理学研究院, 教授 (00291295)
萩谷 昌己 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | model checking / software / liveness |
|---|
| Outline of Final Research Achievements |
Software model checking is a method to verify that software works properly. When verifying a liveness property, a naive method would search the synchronous product of a Buchi automaton created from a LTL formula and a state space. This method is not very effective, because a same state can be created many times. In this research, we propose a method that reduces the average cost of transition by saving and restoring states, and implemented it on Java PathFinder.
|
| Free Research Field |
ソフトウェア工学
|
| Academic Significance and Societal Importance of the Research Achievements |
ソフトウェアモデル検査は，安全性性質の検証には多くの場面で用いられており，プログラムの誤りを見つけることに役立っている．しかし，活性性質の検証事例は比較的少数である．この理由のひとつは性質記述の難しさ，もうひとつには計算量の大きさである．本研究は，Java Pathfinderというひとつのモデル検査器上での実装ではあるが，問題の後者の側面を改善するものである．
|
