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.
-
Using Software Model Checking for Software Certification
Taleghani, Ali (University of Waterloo, 2010-09-13)Software certification is defined as the process of independently confirming that a system or component complies with its specified requirements and is acceptable for use. It consists of the following steps: (1) the ... -
Automated Analysis of Unified Modeling Language (UML) Specifications
Tanuan, Meyer C. (University of Waterloo, 2001)The Unified Modeling Language (UML) is a standard language adopted by the Object Management Group (OMG) for writing object-oriented (OO) descriptions of software systems. UML allows the analyst to add class-level and ... -
Applications of Description Logic and Causality in Model Checking
Ben-David, Shoham (University of Waterloo, 2009-06-19)Model checking is an automated technique for the verification of finite-state systems that is widely used in practice. In model checking, a model M is verified against a specification $\varphi$, exhaustively checking ...