Parametric trace expressions are a formalism expressly designed for parametric runtime verification (RV) which has been introduced and successfully employed in the context of runtime monitoring of multiagent systems. Trace expressions are built on the general notion of event type, which allows them to be adopted in different contexts. In this paper we show how trace expressions can be used for conveniently specifying the expected behavior of a Java-like program to be monitored at runtime. Furthermore, we investigate the basic properties of the primitive operators on which trace expressions are coinductively defined in terms of a labeled transition system; this provides a basis for formal reasoning about equivalence of trace expressions and for adopting useful optimization techniques to speed up runtime verification.

Parametric trace expressions for runtime verification of Java-like programs

ANCONA, DAVIDE;FERRANDO, ANGELO;FRANCESCHINI, LUCA;MASCARDI, VIVIANA
2017-01-01

Abstract

Parametric trace expressions are a formalism expressly designed for parametric runtime verification (RV) which has been introduced and successfully employed in the context of runtime monitoring of multiagent systems. Trace expressions are built on the general notion of event type, which allows them to be adopted in different contexts. In this paper we show how trace expressions can be used for conveniently specifying the expected behavior of a Java-like program to be monitored at runtime. Furthermore, we investigate the basic properties of the primitive operators on which trace expressions are coinductively defined in terms of a labeled transition system; this provides a basis for formal reasoning about equivalence of trace expressions and for adopting useful optimization techniques to speed up runtime verification.
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Tipologia: Documento in Post-print
Dimensione 307.85 kB
Formato Adobe PDF
307.85 kB Adobe PDF Visualizza/Apri

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/876390
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? ND
social impact