By the same authors

From the same journal

Model checking of state-rich formalism Circus by linking to CSP∥B

Research output: Contribution to journalArticle

Full text download(s)

Published copy (DOI)



Publication details

JournalInternational Journal on Software Tools for Technology Transfer
DateE-pub ahead of print - 3 Nov 2015
DatePublished (current) - 1 Feb 2017
Issue number1
Number of pages24
Pages (from-to)73-96
Early online date3/11/15
Original languageEnglish


Since state-rich formalism [Figure not available: see fulltext.] is a combination of Z, CSP, refinement calculus and Dijkstra’s guarded commands, its model checking is intrinsically more complicated and difficult than that of individual state-based languages or process algebras. Current solutions translate executable constructs of [Figure not available: see fulltext.] programs to Java with JCSP, or translate them to CSP processes. Data aspects of [Figure not available: see fulltext.] programs are expressed in the Java programming language or as CSP processes. Both of them have disadvantages. This work presents a new approach to model-checking [Figure not available: see fulltext.] by linking it to CSP‖ B; then we utilise ProB to model-check and animate the CSP‖ B program. The most significant advantage of this approach is the direct mapping of the state part in [Figure not available: see fulltext.] to Z and finally to B, which maintains the high-level abstraction of data specification. In addition, introduction of deadlock, invariant violation checking, LTL formula checking and animation is another key advantage. We present our approach, a link definition for a subset of [Figure not available: see fulltext.] constructs, as well as a popular case study (reactive buffer) to show the practical usability of our work. We conclude with a discussion of related work, advantages and potential limitations of our approach and future work.

Bibliographical note

© Springer-Verlag Berlin Heidelberg 2015. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.

    Research areas

  • B, Buffer, CSP, CSP‖ B, Model checking, ProB, Z, [InlineEquation not available: see fulltext.]

Discover related content

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

View graph of relations