2022 Fiscal Year Final Research Report
Efficient methods of operating omega-automata and its applications to specification verification
| Project/Area Number |
18K18028
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Takushoku University (2019-2022)
Tokyo Institute of Technology (2018) |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Keywords | ωオートマトン / 仕様検証 |
|---|
| Outline of Final Research Achievements |
Formal specification verification can detect errors that are difficult to find manually. However, its computation cost is high. In this research, we aimed at reducing the cost of verification for reactive system specifications, that does not restrict the syntax of specifications or checking properties, and we worked on the following: (1) We proposed efficient methods for operating ω-automata and infinite games, that are the foundations of verification for reactive system specifications. Specifically, we gave a method for simplifying infinite games, and implementation methods for operating ω-automata and infinite games, using partially symbolic techniques. (2) We developed a verification tool, that is based on the proposed methods.
|
| Free Research Field |
システム検証
|
| Academic Significance and Societal Importance of the Research Achievements |
形式仕様の自動検証はその有効性は認識されているものの，計算コストの高さからごく小規模な対象にその適用は限られている．特にリアクティブシステム仕様の自動検証では，理論的基盤として用いられるωオートマトンや無限ゲームの処理が煩雑であることから，その問題は顕著である．本研究では，そのような計算コストの問題を緩和させるため，いくつかの効率化手法を提案した．その成果はリアクティブシステム仕様の自動検証のより大規模で実際的な対象への適用に寄与するものと考えている．
|
