Cavalcanti, Ana; Huang, Wen-ling; Peleska, Jan; Woodcock, Jim CSP and Kripke structures. (English) Zbl 1471.68135 Leucker, Martin (ed.) et al., Theoretical aspects of computing – ICTAC 2015. 12th international colloquium, Cali, Colombia, October 29–31, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9399, 505-523 (2015). Summary: A runtime verification technique has been developed for CSP via translation of CSP models to Kripke structures. With this technique, we can check that a system under test satisfies properties of traces and refusals of its CSP model. This complements analysis facilities available for CSP and for all languages with a CSP-based semantics: Safety-Critical Java, Simulink, SysML, and so on. Soundness of the verification depends on the soundness of the translation and on the traceability of the Kripke structure analysis back to the CSP models and to the property specifications. Here, we present a formalisation of soundness by unifying the semantics of the languages involved: normalised graphs used in CSP model checking, action systems, and Kripke structures. Our contributions are the unified semantic framework and the formal argument itself.For the entire collection see [Zbl 1326.68024]. Cited in 1 Document MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 03B70 Logic in computer science 68N15 Theory of programming languages 68Q55 Semantics in the theory of computing Keywords:semantic models; UTP; formal testing; runtime verification Software:FDR3; SafeJML PDFBibTeX XMLCite \textit{A. Cavalcanti} et al., Lect. Notes Comput. Sci. 9399, 505--523 (2015; Zbl 1471.68135) Full Text: DOI