Can determinism and compositionality coexist in RML?

Davide Ancona
(DIBRIS, University of Genova, Italy)
Angelo Ferrando
(University of Manchester, UK)
Viviana Mascardi
(DIBRIS, University of Genova, Italy)

Runtime verification (RV) consists in dynamically verifying that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specification of its expected properties. RML (Runtime Monitoring Language) is a simple but expressive Domain Specific Language for RV; its semantics is based on a trace calculus formalized by a deterministic rewriting system which drives the implementation of the interpreter of the monitors generated by the RML compiler from the specifications. While determinism of the trace calculus ensures better performances of the generated monitors, it makes the semantics of its operators less intuitive. In this paper we move a first step towards a compositional semantics of the RML trace calculus, by interpreting its basic operators as operations on sets of instantiated event traces and by proving that such an interpretation is equivalent to the operational semantics of the calculus.

In Ornela Dardha and Jurriaan Rot: Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics (EXPRESS/SOS 2020), Online, 31 August 2020, Electronic Proceedings in Theoretical Computer Science 322, pp. 13–32.
Published: 27th August 2020.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: