Loading...
Thumbnail Image
Item

On the computation of counterexamples in compositional nonblocking verification

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 solutions, and experimental results show that counterexamples can be computed successfully for several industrial-scale systems.
Type
Journal Article
Type of thesis
Series
Citation
Malik, R., & Ware, S. (2020). On the computation of counterexamples in compositional nonblocking verification. Discrete Event Dynamic Systems: Theory and Applications. https://doi.org/10.1007/s10626-019-00305-w
Date
2020
Publisher
Springer
Degree
Supervisors
Rights
This is a post-peer-review, pre-copyedit version of an article published in Discrete Event Dynamic Systems: Theory and Applications. The final authenticated version is available online at: 10.1007/s10626-019-00305-w