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.

The early bird catches the worm: First verify, then monitor! / Ferrando, Angelo. - In: SCIENCE OF COMPUTER PROGRAMMING. - ISSN 0167-6423. - 172:(2019), pp. 160-179. [10.1016/j.scico.2018.11.008]

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

Angelo Ferrando
2019

Abstract

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.
2019
172
160
179
The early bird catches the worm: First verify, then monitor! / Ferrando, Angelo. - In: SCIENCE OF COMPUTER PROGRAMMING. - ISSN 0167-6423. - 172:(2019), pp. 160-179. [10.1016/j.scico.2018.11.008]
Ferrando, Angelo
File in questo prodotto:
Non ci sono file associati a questo prodotto.
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/1331881
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 4
social impact