By the same authors

Rapid Prototyping of a Semantically Well Founded Circus Model Checker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published copy (DOI)

Author(s)

Department/unit(s)

Publication details

Title of host publicationSoftware Engineering and Formal Methods
DatePublished - 2014
Pages235-249
PublisherSPRINGER
EditorsDimitra Giannakopoulou, Gwen Salaün
Volume8702
Original languageEnglish
ISBN (Print)978-3-319-10430-0

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume8702
ISSN (Print)978-3-319

Abstract

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 nondeterminism 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.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations