Abstract
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 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 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 models.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
A non-deterministic choice of values means that the bindings are picked randomly among the possible combinations of bindings.
- 3.
The files used in this experiment can be found in the tool repository at https://bit.ly/2ONnk2T.
- 4.
The tests were performed using Intel Core i7 2.8 GHz CPU with 16GB of RAM.
- 5.
References
Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)
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). https://doi.org/10.1007/978-3-319-33600-8_29
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). http://portal.acm.org/citation.cfm?doid=1943628.1943675
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 2016
Boulgakov, A., Gibson-Robinson, T., Roscoe, A.W.: Computing maximal weak and other bisimulations. Form. Asp. Comput. 28(3), 381–407 (2016). https://doi.org/10.1007/s00165-016-0366-2
Cavalcanti, A., Woodcock, J.C.P.: ZRC - a refinement calculus for Z. Form. Asp. Comput. 10(3), 267–289 (1998). http://link.springer.com/10.1007/s001650050016, https://doi.org/10.1007/s001650050016
Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A refinement strategy for Circus. Form. Asp. Comput. 15, 146–181 (2003). https://doi.org/10.1007/s00165-003-0006-5
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). https://doi.org/10.1007/978-3-642-33826-7_24
CZT Partners: Community Z tools, October 2006. czt.sourceforge.net/
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975). http://portal.acm.org/citation.cfm?doid=360933.360975%5Cn
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). https://doi.org/10.1007/978-3-319-14806-9_2
Freitas, L.: Model checking Circus. Ph.D. thesis, Department of Computer Science, The University of York, UK (2005)
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). https://doi.org/10.1007/978-3-319-68270-9_1
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). http://www.cs.ox.ac.uk/projects/fdr/manual/
Gomes, A.O.: Formal Specification of the ARINC 653 Architecture Using Circus (2012). http://etheses.whiterose.ac.uk/id/eprint/2683
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). https://doi.org/10.1007/978-3-319-33600-8_34
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). https://doi.org/10.1007/978-3-642-05089-3_44
Hoare, C., He, J.: Unifying Theories of Programming. Prentice-Hall, Upper Saddle River (1998)
Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation - International Edition, 2nd edn. Addison-Wesley, Boston (2003)
ISO/IEC: ISO/IEC 13568:2002 Information Technology - Z formal specification notation - Syntax, type system and semantics. Technical report (2002). http://standards.iso.org/ittf/PubliclyAvailableStandards/c021573_ISO_IEC_13568_2002(E).zip
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). https://doi.org/10.1007/978-3-642-24485-8_48
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). https://doi.org/10.1007/978-3-540-45236-2_46
Morgan, C.: Programming from Specifications. Prentice Hall International Series in Computer Science, vol. 16, 2nd edn. Prentice Hall, Upper Saddle River (1994). https://dl.acm.org/citation.cfm?id=184737
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). https://doi.org/10.1007/978-3-319-10431-7_17
Nogueira, S., Sampaio, A., Mota, A.: Test generation from state based use case models. Form. Asp. Comput. 26(3), 441–490 (2014)
Oliveira, D., Oliveira, M.V.M.: Joker: an animation framework for formal specications. In: SBMF 2011 - Short Papers, pp. 43–48. ICMC/USP, September 2011
Oliveira, M.V.M.: formal derivation of state-rich reactive programs using Circus. Ph.D. thesis, University of York, UK (2005). http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.428459
Oliveira, M.V.M., Cavalcanti, A., Woodcock, J.C.P.: Unifying theories in ProofPower-Z. Form. Asp. Comput. 25, 133–158 (2013). https://doi.org/10.1007/s00165-007-0044-5
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). http://www.compass-research.eu/Project/Deliverables/D241.pdf
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). https://doi.org/10.1007/978-3-319-10181-1_3
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). https://doi.org/10.1007/978-3-540-73210-5_25
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1973)
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). https://doi.org/10.1007/3-540-60630-0_7
Saaltink, M., Meisels, I., Saaltink, M.: The Z/EVES reference manual (for version 1.5). Reference manual, ORA Canada, pp. 72–85 (1997). http://dl.acm.org/citation.cfm?id=647282.722913
Scattergood, B.: The semantics and implementation of machine-readable CSP, pp. 1–179 (1998). http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.299037
Schneider, S.: Concurrent and Real-Time Systems. Wiley, Chichester (2000)
Woodcock, J.C.P., Bryans, J., Canham, S., Foster, S.: The COMPASS modelling language: timed semantics in UTP, pp. 1–32 (2014)
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)
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). https://doi.org/10.1007/11526841_17
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)
Ye, K.: Model checking of state-rich formalisms. Ph.D. thesis, University of York (2016)
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). https://doi.org/10.1007/s10009-015-0402-1
Acknowledgments
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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Gomes, A.O., Butterfield, A. (2019). Towards a Model-Checker for Circus. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-30942-8_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30941-1
Online ISBN: 978-3-030-30942-8
eBook Packages: Computer ScienceComputer Science (R0)