caa a22 4500 605516294 CHVBK 20210128100713.0 cr unu---uuuuu 210128e20151101xx s 000 0 eng 10.1007/s00165-015-0342-2 doi (NATIONALLICENCE)springer-10.1007/s00165-015-0342-2 Model checking CML: tool development and industrial applications [Elektronische Daten] [A. Mota, A. Farias, J. Woodcock, P. Larsen] 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}$$ M ⊧ 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. British Computer Society, 2015 CML nationallicence Model checker nationallicence Analysis nationallicence FORMULA nationallicence Operational semantics nationallicence SMT nationallicence Mota A. Centro de Informática, Federal University of Pernambuco, Av. Jornalista Anibal Fernandes, s/n-Cidade Universitária, CEP 50.740-560, Recife, PE, Brazil aut Farias A. Federal University of Campina Grande, Campina Grande, Brazil aut Woodcock J. University of York, York, UK aut Larsen P. Aarhus University, Aarhus, Denmark aut Formal Aspects of Computing Springer London 27/5-6(2015-11-01), 975-1001 0934-5043 27:5-6<975 2015 27 165 https://doi.org/10.1007/s00165-015-0342-2 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-015-0342-2 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Mota A. Centro de Informática, Federal University of Pernambuco, Av. Jornalista Anibal Fernandes, s/n-Cidade Universitária, CEP 50.740-560, Recife, PE, Brazil aut NATIONALLICENCE 700 1- Farias A. Federal University of Campina Grande, Campina Grande, Brazil aut NATIONALLICENCE 700 1- Woodcock J. University of York, York, UK aut NATIONALLICENCE 700 1- Larsen P. Aarhus University, Aarhus, Denmark aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/5-6(2015-11-01), 975-1001 0934-5043 27:5-6<975 2015 27 165