Improvements to Transitive-Closure-based Model Checking in Alloy

Abstract

Model checking, which refers to the verification of temporal properties of a transition system, is a common formal method for verifying models. Transitive-closure-based model checking (TCMC), developed by Vakili et al., is a symbolic representation of the semantics of computational tree logic with fairness constraints (CTLFC) for finite models in first-order logic with transitive closure (FOLTC). TCMC is an expression of the complete (i.e., unbounded) model checking problem for CTLFC as a set of constraints in FOLTC without induction, iteration, or invariants. TCMC has been implemented in the Alloy Analyzer.

This thesis focuses on improving practical aspects of using TCMC in Alloy. We provide style guidelines for writing concise declarative models of transition systems for behavioural analysis in Alloy without any extensions to the Alloy language. We address the issue of spurious instances produced when generating instances at small scopes using the Alloy Analyzer by introducing significance axioms, which ensure the instance contains interesting behaviour. We define scoped TCMC for a state scope of n, where n is less than the size of the reachable state space, as the model checking of all transition system instances of state size n that satisfy the transition relation. By considering infinite and finite paths of a transition system separately, we can make useful deductions about the complete model checking problem from the results of scoped TCMC for certain categories of properties. The significant scope, derived from the significance axioms, provides a measure independent of computing resource limitations that a significant part of the state space has been verified, providing higher confidence in the deductions from scoped TCMC.

We present case studies that demonstrate the claims and results of this work. We also compare TCMC in Alloy to NuSMV and bounded model checking in terms of modelling practices, expressibility of temporal properties, model checking results, and performance.