Transitive-closure-based model checking (TCMC) in Alloy

Loading...
Thumbnail Image

Date

2020-01-03

Authors

Farheen, Sabria
Day, Nancy A.
Vakili, Amirhossein
Abbassi, Ali

Advisor

Journal Title

Journal ISSN

Volume Title

Publisher

Springer

Abstract

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 closure (FOLTC). TCMC is an expression of the complete model checking problem for CTLFC as a set of constraints in FOLTC without induction, iteration, or invariants. We implement TCMC in the Alloy Analyzer, showing how a transition system can be expressed declaratively and concisely in the Alloy language. Since the total state space is rarely representable due to the state-space explosion problem, we present scoped TCMC where the property is checked for state spaces of a size smaller than the total state space. We address the problem of spurious instances and carefully describe the meaning of results from scoped TCMC with respect to the complete model checking problem. Using case studies, we demonstrate scoped TCMC and compare it with bounded model checking, highlighting how TCMC can check infinite paths.

Description

This is a post-peer-review, pre-copyedit version of an article published in Software and Systems Modeling. The final authenticated version is available online at: https://doi.org/10.1007/s10270-019-00763-8

Keywords

symbolic model checking, alloy, declarative models

LC Subject Headings

Citation