Abstract
A model checker is an automatic tool that traverses a specific structure (normally a Kripke structure referred as the model M) to check the satisfaction of some (temporal) logical property f. This is formally stated as \({M \models f}\). For some formal notations, the model M of a specification S (written in a formal language L) can be described as a labelled transition system (LTS). Specifically, it is not clear in general how usual tools such as SPIN, FDR, PAT, etc., create the LTS representation from a given process. Although one expects the coherence of the LTS generation with the semantics of L, it is completely hidden inside the model checker itself. In this paper we show how to create a model checker for L, using a development approach based on its operational semantics. We use a systematic semantics embedding and the formal modeling using logic programming and analysis (FORMULA) framework to this end. We illustrate our strategy considering the formal language COMPASS modelling language (CML)—a new language that was based on CSP, VDM and the refinement calculus proposed for modelling and analysis of systems of systems. As FORMULA is based on satisfiability modulo theories solving, our model checker can handle communications and predicates involving data with infinite domains by building and manipulating a symbolic LTS. This goes beyond the capabilities of traditional CSP model checkers such as FDR and PAT. Moreover, we show how to reduce time and space complexities by simple semantic modifications in the embedding. This allows a more semantics-preserving tuning. Finally, we show a real implementation of our model checker in an integrated development platform for CML and its practical use on an industrial case study.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Alberti F, Bruttomesso R, Ghilardi S, Ranise S, Sharygina N (2013) Reachability modulo theory library (extended abstract). In: Fontaine P, Goel A (eds) SMT 2012. EPiC Series, vol 20. EasyChair, pp 67–76
Abrial JR (1996) The B-book. Cambridge University Press, Cambridge
Andrews Z, Didier A, Payne R, Ingram C, Holt J, Perry S, Oliveira M, Woodcock J, Mota A, Romanovsky A (2013) Report on timed fault tree analysis—fault modelling. Technical report D24.2, COMPASS
Andrews Z, Payne R, Romanovsky A, Didier A, Mota A (2013) Model-based development of fault tolerant systems of systems. In: IEEE international systems conference (SysCon), pp 356–363. doi:10.1109/SysCon.2013.6549906
Bryans J, Galloway A, Woodcock J (2012) CML definition 1. Technical report, COMPASS deliverable, D23.2
Baier C, Katoen J-P (2008) Principles of model checking (representation and mind series). The MIT Press, USA
Bjørner N, McMillan K, Rybalchenko A (2012) Program verification as satisfiability modulo theories. In: Fontaine P, Goel A (eds) SMT@IJCAR. EPiC Series, vol 20. EasyChair, pp 3–11
Bryant RE (1992) Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3): 293–318. doi:10.1145/136035.136043
Clarke E, Grumberg O, Long D (1994) Model checking and abstraction. ACM Trans Program Lang Syst 16(5): 1512–1542
Coleman JW, Malmos AK, Couto LD, Larsen PG, Payne R, Foster S, Schulze U, Cajueiro A (2014) Fourth release of the COMPASS tool—Symphony IDE user manual. Technical report D31.4a, COMPASS deliverable, D31.4a
Coleman JW, Malmos AK, Larsen PG, Peleska J, Hains R, Andrews Z, Payne R, Foster S, Miyazawa A, Bertolini C, Didier A (2012) COMPASS tool vision for a system of systems collaborative development environment. In: IEEE SoSE, pp 451–456
Cavalcanti A, Woodcock J (2013) CML definition 3—Timed Operational semantics. Technical report D23.4b, COMPASS deliverable, D23.4b. http://www.compass-research.eu/Project/Deliverables/D234b.pdf. Accessed 24 Aug 2015
Damasceno A, Farias A, Mota A (2009) A mechanized strategy for safe abstraction of CSP specifications. In: SBMF, pp 118–133. doi:10.1007/978-3-642-10452-7_9
Dong JS, Hao P, Sun J, Zhang X (2006) A reasoning method for timed CSP based on constraint solving. In: Zhiming L, Jifeng H (eds) Formal methods and software engineering. Lecture notes in computer science, vol 4260. Springer, Berlin, pp 342–359
De Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems. LNCS, vol 4963. Springer, Berlin, pp 337–340
De Moura L, Bjørner N (2011) Satisfiability modulo theories: introduction and applications. Commun ACM 54(9): 69–77
Fitzgerald JS, Larsen PG, Verhoef M (2008) Vienna development method. In: Wah B (ed) Wiley encyclopedia of computer science and engineering. Wiley, New York
Fitzgerald J, Larsen P, Woodcock J (2014) Foundations for model-based engineering of systems of systems. In: Aiguier M (eds) Complex systems design and management. Springer, Berlin, pp 1–19
Farias A, Mota AC, Sampaio A (2008) Compositional abstraction of CSPZ processes. J Braz Comput Soc 14(2): 23–44
Gallardo MDM, Merino P (1999) A framework for automatic construction of abstract promela models. In: Dams D, Gerth R, Leue S, Massink M (eds) Theoretical and practical aspects of SPIN model checking. Lecture notes in computer science, vol 1680. Springer, Berlin, pp 184–199
Godefroid P (1991) Using partial orders to improve automatic verification methods. In: Proceedings of the 2nd international workshop on computer aided verification (CAV’90), London. Springer, Berlin, pp 176–185
Hoare CAR, He J (1998) Unifying theories of programming. In: Hoare CAR, Bird R (eds) Series in computer science. Prentice Hall, USA
Jackson EK, Kang E, Dahlweid M, Seifert D, Santen T (2010) Components, platforms and possibilities: towards generic automation for MDA. In: EMSOFT, pp 39–48
Jaffar J, Lassez J-L (1987) Constraint logic programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on principles of programming languages (POPL’87). ACM, New York, pp 111–119
Jackson EK, Levendovszky T, Balasubramanian D (2011) Reasoning about metamodeling with formal specifications and automatic proofs. In: MoDELS, pp 653–667
Jackson EK, Seifert D, Dahlweid M, Santen T, Bjørner N, Schulte W (2009) Specifying and composing non-functional requirements in model-based development. In: Bergel A, Fabry J (eds) Software composition. Lecture notes in computer science, vol 5634. Springer, Berlin, pp 72–89. doi:10.1007/978-3-642-02655-3_7
Leuschel M, Butler M (2003) ProB: A model checker for B. In: Araki K, Stefania G, Mandrioli D (eds) FME 2003: formal methods. LNCS, vol 2805. Springer, Berlin, pp 855–874
Lee S (1985) On executable models for rule-based prototyping. In: Proceedings of the 8th international conference on software engineering (ICSE’85). IEEE Computer Society Press, pp 210–215
Leuschel M (2001) Design and implementation of the high-level specification language CSP(LP). In: PADL. LNCS, vol 1990. Springer, Berlin, pp 14–28
Leuschel M, Fontaine M (2008) Probing the depths of CSP-M: a new FDR-compliant validation tool. In: Liu S, Maibaum T, Araki K (eds) Formal methods and software engineering. Lecture notes in computer science, vol 5256. Springer, Berlin, pp 278–297
Lausdahl K, Nielsen CB, Kristensen K (2014) Including running system implementations in the simulation of system of systems models. In: Formal methods: foundations and applications. Lecture notes in computer science. Springer, Berlin
Liu Y, Sun J, Dong JS (2011) PAT 3: an extensible architecture for building multi-domain model checkers. In: Dohi T, Cukic B (eds) IEEE 22nd international symposium on software reliability engineering (ISSRE’11). IEEE, pp 190–199
Mota A, Farias A (2013) COMPASS tool—model checking support. Technical report, COMPASS deliverable, D33.1. http://www.compass-research.eu/Project/Deliverables/D331.pdf. Accessed 24 Aug 2015
Mota A, Farias A (2013) Implementing an SMT-based model checker for CSP from its operational semantics. In: Proceedings of the 16th Brasilian symposium on formal methods (SBMF’13), pp 36–41
Mota A, Farias A (2014) A rapid approach for building a semantically well founded circus model checker. In: Proceedings of the XXI tools session of the Brazilian conference on software (CBSoft’14), pp 77–84
Mota A, Farias A, Didier A, Woodcock J (2014) Rapid prototyping of a semantically well founded circus model checker. In: Giannakopoulou D, Salaün G (eds) Software engineering and formal methods. Lecture notes in computer science, vol 8702. Springer International Publishing, Berlin, pp 235–249. doi:10.1007/978-3-319-10431-7_17
Peled D (1993) All from one, one for all: on model checking using representatives. In: Courcoubetis C (ed) Computer aided verification. Lecture notes in computer science, vol 697. Springer, Berlin, pp 409–423
Plotkin GD (2004) A structural approach to operational semantics. J Log Algebr Program 60–61:17–139
Palikareva H, Ouaknine J, Roscoe AW (2012) SAT-solving in CSP trace refinement. Sci Comput Program 77(10–11): 1178–1197
Papadopoulos Y, Walker M, Parker D, Rüde E, Hamann R, Uhlig A, Grätz U, Lien R (2011) Engineering failure analysis and design optimisation with HiP-HOPS. Eng Fail Anal 18: 590–608
Roscoe AW (1998) The theory and practice of concurrency. Prentice Hall, USA. The text book teaching material can be found at http://www.cs.ox.ac.uk/people/bill.roscoe/publications/68b.pdf. Accessed 24 Aug 2015
Roscoe AW (2010) Understanding Concurrent Systems. Springer-Verlag New York, Inc., New York, NY, USA, 1st edition
Roşu G, Şerbănuţă TF (2010) An overview of the K semantic framework. J Log Algebraic Program 79(6): 397–434
Sun J, Liu Y, Dong JS, Chen C (2009) Integrating specification and programs for system modeling and verification. In: Chin WN Qin S (eds) TASE 2009, third IEEE international symposium on theoretical aspects of software engineering. IEEE Computer Society, Tianjin, pp 127–135
Schneider S, Treharne H (2002) Communicating B machines. In: Bert D, Bowen JP, Henson MC, Robinson K (eds) ZB 2002: formal specification and development in Z and B. Lecture notes in computer science, vol 2272. Springer, Berlin, pp 416–435
Verdejo A (2000) Implementing and verifying CCS in MAUDE. In: The international federation for information processing (IFIP)
Woodcock J, Cavalcanti A (2002) The semantics of circus. In: Proceedings of the 2nd international conference of B and Z users on formal specification and development in Z and B (ZB’02). Springer, London, pp 184–203
Woodcock JCP, Cavalcanti ALC, Freitas L (2005) Operational semantics for model checking circus. In: Fitzgerald J, Hayes IJ, Tarlecki A (eds) FM 2005: formal methods, international symposium of formal methods Europe. Lecture notes in computer science, vol 3582. Springer, Berlin, pp 237–252
Woodcock J, Cavalcanti A, Fitzgerald J, Larsen P, Miyazawa A, Perry S (2012) Features of CML: a formal modelling language for systems of systems. In: IEEE SoSE
Woodcock J, Miyazawa A (2012) CML definition 0. Public document. Deliverable Number: D23.1, Version: 1.0, COMPASS Project, University of York
Zeyda F, Cavalcanti A, Wellings AJ (2011) The safety-critical Java mission model: a formal account. In: ICFEM, pp 49–65
Author information
Authors and Affiliations
Corresponding author
Additional information
Michael Butler and Cliff Jones
Rights and permissions
About this article
Cite this article
Mota, A., Farias, A., Woodcock, J. et al. Model checking CML: tool development and industrial applications. Form Asp Comp 27, 975–1001 (2015). https://doi.org/10.1007/s00165-015-0342-2
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-015-0342-2