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.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
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