The early bird catches the worm: First verify, then monitor!



Ferrando, A ORCID: 0000-0002-8711-4670
(2019) The early bird catches the worm: First verify, then monitor! Science of Computer Programming, 172. pp. 160-179.

[img] Text
main.pdf - Author Accepted Manuscript

Download (520kB)

Abstract

© 2018 Elsevier B.V. Trace expressions are a compact and expressive formalism, initially devised for runtime verification of agent interactions in multiagent systems, which has been successfully employed to model real-world protocols, and to generate monitors for mainstream multiagent system platforms, and generalized to support runtime verification of different kinds of properties and systems. In this paper, we propose an algorithm to check Linear Temporal Logic (LTL) properties satisfiability on trace expressions. To do this, we show how to translate a trace expression into a Büchi Automaton in order to realize an Automata-Based Model Checking. We show that this translation generates an over-approximation of our trace expression leading us to obtain a sound procedure to verify LTL properties. Once we have statically checked a set of LTL properties, we can conclude that: (1) our trace expression is formally correct (2) since we use this trace expression to generate monitors checking the runtime behavior of the system, the LTL properties verified by this trace expression are also verified by the monitored system.

Item Type: Article
Uncontrolled Keywords: Runtime verification of object-oriented programming, Trace expressions, Automata-based model checking, Runtime monitoring, Combining static and runtime verification
Depositing User: Symplectic Admin
Date Deposited: 11 Feb 2019 09:09
Last Modified: 19 Jan 2023 01:04
DOI: 10.1016/j.scico.2018.11.008
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3032628