Throughout the past decades two schools have been developing formal techniques for correct software development, taking complementary approaches: the model-based approach and the behavioural approach. Combinations of languages from both approaches have also been proposed. The lack of support for refinement of state-rich reactive systems in a calculational style has motivated the creation of Circus, a combination of Z, CSP, and Djikstra's commmand language. In this paper, we foster the reuse of theoretical results underpinned on CSP to Circus by providing a sound mapping for processes and refinement from Circus to CSP. This mapping is proved sound from an existing link between these languages, established in the Unifying Theories of Programming (UTP). Our results allow analysing Circus specifications with techniques and tools, like FDR2 and PAT, originally developed for CSP. We illustrate the overall approach with a running example. © 2014 Springer International Publishing.
CITATION STYLE
Oliveira, M. V. M., Sampaio, A. C. A., & Conserva Filho, M. S. (2014). Model-checking Circus state-rich specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8739 LNCS, pp. 39–54). Springer Verlag. https://doi.org/10.1007/978-3-319-10181-1_3
Mendeley helps you to discover research relevant for your work.