Advertisement

Circus2CSP: A Tool for Model-Checking Circus Using FDR

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

Abstract

In this paper, we introduce Circus2CSP, a tool that automatically translates Circus into \({CSP}_{M}\), with an implementation based on a published manual translation scheme. This scheme includes new and modified translation rules that emerged as a result of experimentation. We addressed issues with FDR state-space explosion, by optimising our models using the Circus Refinement Laws. We briefly describe the usage of Circus2CSP along with a discussion of some experiments comparing our tool with the literature.

Notes

Acknowledgements

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.

References

  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.
    Aeronautical Radio, I.A.: ARINC 653: Avionics Application Standard Software Interface, November 2006Google Scholar
  3. 3.
    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_29CrossRefGoogle Scholar
  4. 4.
    Beg, A., Butterfield, A.: Development of a prototype translator from Circus to CSPm. In: 2015 International Conference on Open Source Systems and Technologies, Proceedings, ICOSST 2015, pp. 16–23, December 2016Google Scholar
  5. 5.
    Boulgakov, A., Gibson-Robinson, T., Roscoe, A.W.: Computing maximal weak and other bisimulations. Formal Aspects Comput. 28(3), 381–407 (2016).  https://doi.org/10.1007/s00165-016-0366-2MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Cavalcanti, A., Woodcock, J.C.P.: ZRC - a refinement calculus for Z. Formal Aspects Comput. 10(3), 267–289 (1998).  https://doi.org/10.1007/s001650050016CrossRefzbMATHGoogle Scholar
  7. 7.
    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%5CnMathSciNetCrossRefGoogle Scholar
  8. 8.
    Freitas, L.: Model checking circus. Ph.D. thesis, Department of Computer Science, The University of York, UK (2005)Google Scholar
  9. 9.
    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). https://www.cs.ox.ac.uk/projects/fdr/manual/CrossRefGoogle Scholar
  10. 10.
    Gomes, A.O.: Formal Specification of the ARINC 653 Architecture Using Circus (2012). https://etheses.whiterose.ac.uk/id/eprint/2683
  11. 11.
    Gomes, A.O.: Model-checking circus with FDR using Circus2CSP. Ph.D. thesis, Trinity College Dublin (2019). https://www.tara.tcd.ie/handle/2262/86009
  12. 12.
    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_34CrossRefGoogle Scholar
  13. 13.
    Gomes, A.O., Butterfield, A.: Circus2CSP - a translator from circus to CSPm (2018). https://bitbucket.org/circusmodelcheck/circus2csp
  14. 14.
    Gomes, A.O., Butterfield, A.: Towards a model-checker for circus. In: 3rd World Congress on Formal Methods. Springer, Berlin (2019)Google Scholar
  15. 15.
    Hoare, C., He, J.: Unifying Theories of Programming. Prentice-Hall, Upper Saddle River (1998)zbMATHGoogle Scholar
  16. 16.
    Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation - International Edition, 2nd edn. Addison-Wesley, Boston (2003)Google Scholar
  17. 17.
    Hopkins, D., Roscoe, A.W.: SVA, a tool for analysing shared-variable programs. Electronic Notes in Theoretical Computer Science, pp. 1–5 (2007). https://www.cs.ox.ac.uk/people/bill.roscoe/publications/119.pdf
  18. 18.
    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_48CrossRefGoogle Scholar
  19. 19.
    Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)CrossRefGoogle Scholar
  20. 20.
    Lowe, G.: Specification of communicating processes: temporal logic versus refusals-based refinement. Formal Aspects Comput. 20(3), 277–294 (2008). https://link.springer.com/content/pdf/10.1007%2Fs00165-007-0065-0.pdfCrossRefGoogle Scholar
  21. 21.
    Malik, P., Utting, M.: CZT: a framework for Z tools. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 65–84. Springer, Heidelberg (2005).  https://doi.org/10.1007/11415787_5. http://czt.sourceforge.netCrossRefGoogle Scholar
  22. 22.
    Morgan, C.: Programming from Specifications. Prentice Hall International Series in Computer Science, 2nd edn. vol. 16. Prentice Hall (1994). https://dl.acm.org/citation.cfm?id=184737
  23. 23.
    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_17CrossRefGoogle Scholar
  24. 24.
    Nogueira, S., Sampaio, A., Mota, A.: Test generation from state based use case models. Formal Aspects Comput. 26(3), 441–490 (2014)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Oliveira, M.V.M.: Formal derivation of state-rich reactive programs using circus. Ph.D. thesis, University of York, UK (2005). https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.428459
  26. 26.
    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). https://www.compass-research.eu/Project/Deliverables/D241.pdf
  27. 27.
    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_3CrossRefGoogle Scholar
  28. 28.
    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_25CrossRefGoogle Scholar
  29. 29.
    Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1973)Google Scholar
  30. 30.
    Saaltink, M., Meisels, I., Saaltink, M.: The Z/EVES Reference Manual (for Version 1.5). Reference Manual, ORA Canada, pp. 72–85 (1997). https://dl.acm.org/citation.cfm?id=647282.722913
  31. 31.
    Schneider, S.: Concurrent and Real-Time Systems. Wiley, Chichester (2000)Google Scholar
  32. 32.
    Utting, M.: Jaza User Manual and Tutorial, June 2005Google Scholar
  33. 33.
    Woodcock, J., Cavalcanti, A.: The semantics of circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45648-1_10CrossRefGoogle Scholar
  34. 34.
    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_17CrossRefGoogle Scholar
  35. 35.
    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
  36. 36.
    Ye, K.: Model checking of state-rich formalisms. Ph.D. thesis, University of York (2016)Google Scholar
  37. 37.
    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

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 DublinDublinIreland

Personalised recommendations