×

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].

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

Software:

FDR3; SafeJML
PDFBibTeX XMLCite
Full Text: DOI