Counterexample Computation in Compositional Nonblocking Verification
Citation
Export citationMalik, R., & Ware, S. (2018). Counterexample Computation in Compositional Nonblocking Verification. In IFAC PapersOnLine (Vol. 51, pp. 416–421). Elsevier. https://doi.org/10.1016/j.ifacol.2018.06.334
Permanent Research Commons link: https://hdl.handle.net/10289/12563
Abstract
This paper describes algorithms to compute a counterexample when compositional nonblocking verification determines that a discrete event system is blocking. Counterexamples are an important feature of model checking that explains the cause of a detected problem, greatly helping users to understand and fix faults. In compositional verification, counterexamples are difficult to compute due to the large state space and the loss of information after abstraction. The paper explains the difficulties and proposes a solution, and experimental results show that counterexamples can be computed successfully for several industrial-scale systems.
Date
2018Publisher
Elsevier
Rights
This is the author's accepted version. © 2018, IFAC (International Federation of Automatic Control) Hosting by Elsevier Ltd.