A Tool for Model Checking Eventual Model Checking in a Stratified Way
Moe Nandi Aung, Yati Phyo, Canh Minh, Kazuhiro Ogata · 2022 9th International Conference on Dependable Systems and Their Applications (DSA) · 2022
We present a tool for model checking eventual properties in a stratified w ay t hat c an e ase t he n otorious s tate space explosion problem. As shown by the name, the tool is dedicated to eventual properties formalized as$\diamond\varphi$where$\varphi$is a state proposition. It is possible to formalize crucial requirements/properties that should be satisfied by a lot of software systems. For example, termination is such a requirement/property. Therefore, it is meaningful to concentrate on the properties. We also conduct some case studies showing that the state space explosion can be eased to a certain scope with the technique/tool.