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.. - 2504:(2019), pp. 248-260. (Intervento presentato al convegno 20th Italian Conference on Theoretical Computer Science, ICTCS 2019 tenutosi a ita nel 9 settembre 2019).

A deterministic event calculus for effective runtime verification

Ferrando A.;
2019

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.
2019
20th Italian Conference on Theoretical Computer Science, ICTCS 2019
ita
9 settembre 2019
2504
248
260
Ancona, D.; Franceschini, L.; Ferrando, A.; Mascardi, V.
A deterministic event calculus for effective runtime verification / Ancona, D.; Franceschini, L.; Ferrando, A.; Mascardi, V.. - 2504:(2019), pp. 248-260. (Intervento presentato al convegno 20th Italian Conference on Theoretical Computer Science, ICTCS 2019 tenutosi a ita nel 9 settembre 2019).
File in questo prodotto:
File Dimensione Formato  
main.pdf

Open access

Tipologia: Versione dell'autore revisionata e accettata per la pubblicazione
Dimensione 113.14 kB
Formato Adobe PDF
113.14 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

Licenza Creative Commons
I metadati presenti in IRIS UNIMORE sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono rilasciati con licenza Attribuzione 4.0 Internazionale (CC BY 4.0), salvo diversa indicazione.
In caso di violazione di copyright, contattare Supporto Iris

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