Extracting Counterexamples from Transitive-Closure-Based Model Checking
Abstract
We address the problem of how to extract counterexamples for the transitive-closure-based model checking (TCMC) technique. TCMC is a representation of the CTLFC (CTL with fairness constraints) model checking problem in first-order logic with transitive closure (FOLTC) and has been implemented in the Alloy Analyzer. It is a declarative, symbolic model checking method. As a CTL model checking method, TCMC is defined over transition systems and states (rather than paths) and therefore, returns a transition system with a bug as a counterexample. Our contribution is to isolate a counterexample path/subgraph in a declarative manner by adding constraints that do not depend on the property. Our method does not require extensions to Alloy.
Cite this version of the work
Mitchell Kember, Lynn Tran, George Gao, Nancy Day
(2019).
Extracting Counterexamples from Transitive-Closure-Based Model Checking. UWSpace.
http://hdl.handle.net/10012/15994
Other formats
Related items
Showing items related by title, author, creator and subject.
-
Improvements to Many-Sorted Finite Model Finding using SMT Solvers
Zila, Owen (University of Waterloo, 2023-08-17)Formal modeling is a powerful tool in requirements engineering. By modeling a system before implementation, one can discover bugs before they appear in testing or production. Model finding (or instance finding) for a model ... -
Transitive-closure-based model checking (TCMC) in Alloy
Farheen, Sabria; Day, Nancy A.; Vakili, Amirhossein; Abbassi, Ali (Springer, 2020-01-03)We present transitive-closure-based model checking (TCMC): a symbolic representation of the semantics of computational tree logic with fairness constraints (CTLFC) for finite models in first-order logic with transitive ... -
A Comprehensive Study of Declarative Modelling Languages
Bandali, Amin (University of Waterloo, 2020-07-14)Declarative behavioural modelling is a powerful modelling paradigm that enables users to model system functionality abstractly and formally. An abstract model is a concise and compact representation of key characteristics ...