Model checking CML: tool development and industrial applications. (November 2015)

• Record Type: Journal Article
• Authors: Mota, A.; Farias, A.; Woodcock, J.; Larsen, P.
• Is Part Of: Formal aspects of computing. Volume 27:Number 5(2015)
• Page Start: 975
• Page End: 1001
• Publication Date: 2015-11
• Subjects: CML -- Model checker -- Analysis -- FORMULA -- Operational semantics -- SMT; Computer science -- Periodicals; 004.05
• DOI: 10.1007/s00165-015-0342-2
• Languages: English
• ISSNs: 0934-5043

Abstract

Abstract A model checker is an automatic tool that traverses a specific structure (normally a Kripke structure referred as the modelM ) to check the satisfaction of some (temporal) logical propertyf . This is formally stated as $${M \models f}$$ M ⊧ f . For some formal notations, the modelM of a specificationS (written in a formal languageL ) 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 ofL, it is completely hidden inside the model checker itself. In this paper we show how to create a model checker forL, 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.