Runtime verification (RV) is an approach to verification consisting in dynamically checking that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specification of its expected correct behavior. RML (Runtime Monitoring Language) is a simple but powerful Domain Specific Language (DSL) for RV which is able to express non context-free properties. When designing RML, particular care has been taken to favor abstraction and simplicity, to better support reusability and portability of specifications and interoperability of the monitors generated from them; this is mainly achieved by decoupling the two problems of property specification and event generation, and by minimizing the available primitive constructs. The formalization and implementation of RML is based on a trace calculus with a fully deterministic rewriting semantics. The semantics of RML is defined by translation into such a calculus, which, in fact, is used as intermediate representation (IR) by the RML compiler. The effectiveness of RML and its methodological impact on RV are presented through interesting patterns that can be adapted to different contexts requiring verification of standard properties. A collection of tested examples is provided, together with benchmarks showing that the deterministic semantics and the performed dynamic optimizations based on the laws of the trace calculus significantly improve the performances of the generated monitors.

RML: Theory and practice of a domain specific language for runtime verification

Davide Ancona;Luca Franceschini;Angelo Ferrando;Viviana Mascardi
2021-01-01

Abstract

Runtime verification (RV) is an approach to verification consisting in dynamically checking that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specification of its expected correct behavior. RML (Runtime Monitoring Language) is a simple but powerful Domain Specific Language (DSL) for RV which is able to express non context-free properties. When designing RML, particular care has been taken to favor abstraction and simplicity, to better support reusability and portability of specifications and interoperability of the monitors generated from them; this is mainly achieved by decoupling the two problems of property specification and event generation, and by minimizing the available primitive constructs. The formalization and implementation of RML is based on a trace calculus with a fully deterministic rewriting semantics. The semantics of RML is defined by translation into such a calculus, which, in fact, is used as intermediate representation (IR) by the RML compiler. The effectiveness of RML and its methodological impact on RV are presented through interesting patterns that can be adapted to different contexts requiring verification of standard properties. A collection of tested examples is provided, together with benchmarks showing that the deterministic semantics and the performed dynamic optimizations based on the laws of the trace calculus significantly improve the performances of the generated monitors.
File in questo prodotto:
File Dimensione Formato  
journal-version.pdf

accesso chiuso

Descrizione: Articolo su rivista
Tipologia: Documento in versione editoriale
Dimensione 2.04 MB
Formato Adobe PDF
2.04 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11567/1036613
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 10
social impact