Towards a Model-Checker for Circus

  • Artur Oliveira GomesEmail author
  • Andrew Butterfield
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)


Among several approaches aiming at the correctness of systems, model-checking is one technique to formally assess system models regarding their desired/undesired behavioural properties. We aim at model-checking the Open image in new window notation that combines Z, CSP, and Morgan’s refinement calculus, based on the Unifying Theories of Programming. In this paper, we experiment with approaches for capturing Open image in new window processes in CSP, and for each approach, we evaluate the impact of our decisions on the state-space explored as well as the time spent for such a checking using FDR. We also experimented with the consequences of model-checking CSP models that capture both state invariants and preconditions of Open image in new window models.



This work was funded by CNPq (Brazilian National Council for Scientific and Technological Development) within the Science without Borders programme, Grant No. 201857/2014-6, and partially funded by Science Foundation Ireland grant 13/RC/2094.


  1. 1.
    Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)CrossRefGoogle Scholar
  2. 2.
    Mashkoor, A.: The hemodialysis machine case study. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 329–343. Springer, Cham (2016). Scholar
  3. 3.
    Beg, A., Butterfield, A.: Linking a state-rich process algebra to a state-free algebra to verify software/hardware implementation. In: Proceedings of the 8th International Conference on Frontiers of Information Technology - FIT 2010, pp. 1–5 (2010).
  4. 4.
    Beg, A., Butterfield, A.: Development of a prototype translator from Circus to CSPm. In: Proceedings of ICOSST 2015–2015 International Conference on Open Source Systems and Technologies, pp. 16–23, December 2016Google Scholar
  5. 5.
    Boulgakov, A., Gibson-Robinson, T., Roscoe, A.W.: Computing maximal weak and other bisimulations. Form. Asp. Comput. 28(3), 381–407 (2016). Scholar
  6. 6.
    Cavalcanti, A., Woodcock, J.C.P.: ZRC - a refinement calculus for Z. Form. Asp. Comput. 10(3), 267–289 (1998).,
  7. 7.
    Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A refinement strategy for Circus. Form. Asp. Comput. 15, 146–181 (2003). Scholar
  8. 8.
    Conserva Filho, M., Oliveira, M.V.M.: Implementing tactics of refinement in CRefine. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 342–351. Springer, Heidelberg (2012). Scholar
  9. 9.
    CZT Partners: Community Z tools, October 2006.
  10. 10.
    Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975).
  11. 11.
    Foster, S., Zeyda, F., Woodcock, J.: Isabelle/UTP: a mechanised theory engineering framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 21–41. Springer, Cham (2015). Scholar
  12. 12.
    Freitas, L.: Model checking Circus. Ph.D. thesis, Department of Computer Science, The University of York, UK (2005)Google Scholar
  13. 13.
    Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 3–26. Springer, Cham (2017). Scholar
  14. 14.
    Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 – a modern model checker for CSP. Tools Algorithms Constr. Anal. Syst. 8413, 187–201 (2014).
  15. 15.
    Gomes, A.O.: Formal Specification of the ARINC 653 Architecture Using Circus (2012).
  16. 16.
    Gomes, A.O., Butterfield, A.: Modelling the haemodialysis machine with Circus. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 409–424. Springer, Cham (2016). Scholar
  17. 17.
    Gomes, A.O., Oliveira, M.V.M.: Formal specification of a cardiac pacing system. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 692–707. Springer, Heidelberg (2009). Scholar
  18. 18.
    Hoare, C., He, J.: Unifying Theories of Programming. Prentice-Hall, Upper Saddle River (1998)zbMATHGoogle Scholar
  19. 19.
    Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation - International Edition, 2nd edn. Addison-Wesley, Boston (2003)zbMATHGoogle Scholar
  20. 20.
    ISO/IEC: ISO/IEC 13568:2002 Information Technology - Z formal specification notation - Syntax, type system and semantics. Technical report (2002).
  21. 21.
    Jackson, E.K., Levendovszky, T., Balasubramanian, D.: Reasoning about metamodeling with formal specifications and automatic proofs. In: Whittle, J., Clark, T., Kühne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 653–667. Springer, Heidelberg (2011). Scholar
  22. 22.
    Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). Scholar
  23. 23.
    Morgan, C.: Programming from Specifications. Prentice Hall International Series in Computer Science, vol. 16, 2nd edn. Prentice Hall, Upper Saddle River (1994). Scholar
  24. 24.
    Mota, A., Farias, A., Didier, A., Woodcock, J.: Rapid prototyping of a semantically well founded Circus model checker. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 235–249. Springer, Cham (2014). Scholar
  25. 25.
    Nogueira, S., Sampaio, A., Mota, A.: Test generation from state based use case models. Form. Asp. Comput. 26(3), 441–490 (2014)MathSciNetCrossRefGoogle Scholar
  26. 26.
    Oliveira, D., Oliveira, M.V.M.: Joker: an animation framework for formal specications. In: SBMF 2011 - Short Papers, pp. 43–48. ICMC/USP, September 2011Google Scholar
  27. 27.
    Oliveira, M.V.M.: formal derivation of state-rich reactive programs using Circus. Ph.D. thesis, University of York, UK (2005).
  28. 28.
    Oliveira, M.V.M., Cavalcanti, A., Woodcock, J.C.P.: Unifying theories in ProofPower-Z. Form. Asp. Comput. 25, 133–158 (2013). Scholar
  29. 29.
    Oliveira, M.V.M., Sampaio, A., Antonino, P., Ramos, R., Cavalcanti, A., Woodcock, J.C.P.: Compositional analysis and design of CML models. Technical report D24.1, COMPASS Deliverable (2013).
  30. 30.
    Oliveira, M.V.M., Sampaio, A.C.A., Conserva Filho, M.S.: Model-checking Circus state-rich specifications. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 39–54. Springer, Cham (2014). Scholar
  31. 31.
    Plagge, D., Leuschel, M.: Validating Z specifications using the ProB animator and model checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 480–500. Springer, Heidelberg (2007). Scholar
  32. 32.
    Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1973)Google Scholar
  33. 33.
    Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M.H., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 133–152. Springer, Heidelberg (1995). Scholar
  34. 34.
    Saaltink, M., Meisels, I., Saaltink, M.: The Z/EVES reference manual (for version 1.5). Reference manual, ORA Canada, pp. 72–85 (1997).
  35. 35.
    Scattergood, B.: The semantics and implementation of machine-readable CSP, pp. 1–179 (1998).
  36. 36.
    Schneider, S.: Concurrent and Real-Time Systems. Wiley, Chichester (2000)Google Scholar
  37. 37.
    Woodcock, J.C.P., Bryans, J., Canham, S., Foster, S.: The COMPASS modelling language: timed semantics in UTP, pp. 1–32 (2014)Google Scholar
  38. 38.
    Woodcock, J.C.P., Cavalcanti, A.: The semantics of Circus. In: ZB 2002: formal specification and development in Z and B. In: 2nd International Conference of B and Z Users Grenoble (2002)Google Scholar
  39. 39.
    Woodcock, J., Cavalcanti, A., Freitas, L.: Operational semantics for model checking Circus. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 237–252. Springer, Heidelberg (2005). Scholar
  40. 40.
    Woodcock, J.C.P., Davies, J.: Using Z, Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science. Prentice-Hall Inc., Upper Saddle River (1996)zbMATHGoogle Scholar
  41. 41.
    Ye, K.: Model checking of state-rich formalisms. Ph.D. thesis, University of York (2016)Google Scholar
  42. 42.
    Ye, K., Woodcock, J.C.P.: Model checking of state-rich formalism Circus by linking to CSP——B. Int. J. Softw. Tools Technol. Transf. 19(1), 73–96 (2017). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Universidade Federal de Mato Grosso do SulCorumbáBrazil
  2. 2.School of Computer Science and StatisticsTrinity College DublinDublin 2Ireland

Personalised recommendations