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
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2018: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2017: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2016: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Keywords | model checking / software / liveness / モデル検査 / Java / ソフトウェア / ソフトウェア検証 / アルゴリズム / ソフトウエア学 / 仕様記述・検証 |
|---|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
ソフトウェアモデル検査は，安全性性質の検証には多くの場面で用いられており，プログラムの誤りを見つけることに役立っている．しかし，活性性質の検証事例は比較的少数である．この理由のひとつは性質記述の難しさ，もうひとつには計算量の大きさである．本研究は，Java Pathfinderというひとつのモデル検査器上での実装ではあるが，問題の後者の側面を改善するものである．
|
Report
(4 results)
Research Products
(11 results)
