Rapid Prototyping of a Semantically Well Founded Circus Model Checker

摘要

Nowadays academia and industry use model checkers. These tools use search-based algorithms to check the satisfaction of some property f in M. Formally, M |= f, where M is a transition system representation of a specification written in a language L. Such a representation may come from the semantics of L. This paper presents a rapid prototyping of a model checker development strategy for Circus based on its operational semantics. We capture this semantics with the Microsoft FORMULA framework and use it to analyse (deadlock, livelock, and nondetermin-ism of) Circus specifications. As FORMULA supports SMT-solving, we can handle infinite data communications and predicates. Furthermore, we create a semantically well founded Circus model checker as long as executing FORMULA is equivalent to reasoning with First-Order Logic (Clark completion). We illustrate the use of the model-checker with an extract of an industrial case study.