A deterministic event calculus for effective runtime verification



Ancona, D, Franceschini, L, Ferrando, A ORCID: 0000-0002-8711-4670 and Mascardi, V
(2019) A deterministic event calculus for effective runtime verification. .

[thumbnail of paper28.pdf] Text
paper28.pdf - Published version

Download (280kB) | Preview

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.

Item Type: Conference or Workshop Item (Unspecified)
Divisions: Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User: Symplectic Admin
Date Deposited: 28 May 2021 10:35
Last Modified: 18 Jan 2023 22:37
URI: https://livrepository.liverpool.ac.uk/id/eprint/3124350