Jaksic/Bartocci/Grosu/Nickovic.

An Algebraic Framework for Runtime Verification.*

S. Jaksic, E. Bartocci, R. Grosu, and D. Nickovic.

Runtime verification (RV) is a pragmatic and scalable, yet rigorous technique, to assess the correctness of complex systems, including cyber-physical systems (CPS). Modern RV tools also allow to measure the distance of a CPS behavior from a given formal requirement, thus, to quantify the robustness of a CPS with respect to perturbations caused by the physical environment. In this paper we propose Algebraic Runtime Verification (ARV), a general, semantic framework for correctness and robustness monitoring. ARV implements an abstract monitoring procedure, in which the specification language can be instantiated with various qualitative and quantitative semantics. This allows us to expose the core aspects of RV, by separating the monitoring algorithm from the concrete choice of the specification language and its semantics. We demonstrate the effectiveness of our framework on two examples from the automotive domain.

In Proc. of EMSOFT'18, the International Conference on Embedded Software, Torino, Italy, September, 2018, ACM.

*This work was partially supported by the NSF-Frontiers Cyber-Cardia Award, the US-AFOSR Arrive Award, the EU-Artemis EMC2 Award, the EU-Ecsel Semi40 Award, the EU-Ecsel Productive 4.0 Award, the AT-FWF-NFN RiSE Award, the AT-FWF-LogicCS-DC Award, the AT-FFG Harmonia Award, the AT-FFG Em2Apps Award, and the TUW-CPPS-DK Award.