Runtime verification (RV) is an effective technique for dynamically monitoring, even after deployment, properties that could be hardly verified statically. To this aim, specification formalims for RV have to reconcile expressive power and monitoring efficiency. We present an event calculus which provides a basis for the semantics and the implementation of RML, a domain specific language (DSL) for RV. The semantics of the calculus is based on a deterministic reduction strategy which allows concise specifications of non context-free properties, and their efficient verification at runtime.

A deterministic event calculus for effective runtime verification

Ancona D.;Franceschini L.;Ferrando A.;Mascardi V.
2019-01-01

Abstract

Runtime verification (RV) is an effective technique for dynamically monitoring, even after deployment, properties that could be hardly verified statically. To this aim, specification formalims for RV have to reconcile expressive power and monitoring efficiency. We present an event calculus which provides a basis for the semantics and the implementation of RML, a domain specific language (DSL) for RV. The semantics of the calculus is based on a deterministic reduction strategy which allows concise specifications of non context-free properties, and their efficient verification at runtime.
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Descrizione: Articolo principale
Tipologia: Documento in Post-print
Dimensione 113.14 kB
Formato Adobe PDF
113.14 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/999629
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact