Runtime Verification (RV) basically means monitoring an execution trace of a system under scrutiny and checking if the trace satisfies or violates a specification. In Assumption-Based Runtime Verification (ABRV), runtime monitors may be synthesized from not only the specification but also a system model (either full or partial), which represents the assumptions on which the input traces are expected to follow. With assumptions the monitor can additionally check if the input traces actually follow the assumptions. Some previous research has shown that monitors under assumptions can be more precise or even predictive, while non-monitorable specifications may become monitorable under assumptions. The question of synthesizing runtime monitors for finite-state systems and propositional or first-order temporal logics, with or without assumptions, has mostly been answered by prior work. For monitoring infinite-state systems, however, most existing approaches focus on supporting parametric or first-order specifications while they cannot be easily extended to support assumptions. This paper presents a general solution for ABRV of infinite-state systems by a reduction of RV problems to LTL Model Checking (MC), which is further based on Satisfiability Modulo Theories and other techniques. When First-Order Quantifier Elimination (QE) is also available, the corresponding algorithm can be greatly optimized. This solution is general because in theory any LTL MC (and QE) algorithms can be used, and the supported types of infinite-state variables also depend on these underlying algorithms. In particular, the relatively expensive model checking can be minimized by a modified version of Bounded Model Checking algorithm which performs model checking incrementally on each input of the monitor.

Assumption-Based Runtime Verification of Infinite-State Systems / Cimatti, Alessandro; Tian, Chun; Tonetta, Stefano. - 12974:(2021), pp. 207-227. (Intervento presentato al convegno Runtime Verification 2021 tenutosi a Virtual Event nel 11/10/2021) [10.1007/978-3-030-88494-9_11].

Assumption-Based Runtime Verification of Infinite-State Systems

Cimatti, Alessandro;Tian, Chun;Tonetta, Stefano
2021-01-01

Abstract

Runtime Verification (RV) basically means monitoring an execution trace of a system under scrutiny and checking if the trace satisfies or violates a specification. In Assumption-Based Runtime Verification (ABRV), runtime monitors may be synthesized from not only the specification but also a system model (either full or partial), which represents the assumptions on which the input traces are expected to follow. With assumptions the monitor can additionally check if the input traces actually follow the assumptions. Some previous research has shown that monitors under assumptions can be more precise or even predictive, while non-monitorable specifications may become monitorable under assumptions. The question of synthesizing runtime monitors for finite-state systems and propositional or first-order temporal logics, with or without assumptions, has mostly been answered by prior work. For monitoring infinite-state systems, however, most existing approaches focus on supporting parametric or first-order specifications while they cannot be easily extended to support assumptions. This paper presents a general solution for ABRV of infinite-state systems by a reduction of RV problems to LTL Model Checking (MC), which is further based on Satisfiability Modulo Theories and other techniques. When First-Order Quantifier Elimination (QE) is also available, the corresponding algorithm can be greatly optimized. This solution is general because in theory any LTL MC (and QE) algorithms can be used, and the supported types of infinite-state variables also depend on these underlying algorithms. In particular, the relatively expensive model checking can be minimized by a modified version of Bounded Model Checking algorithm which performs model checking incrementally on each input of the monitor.
2021
Runtime Verification (RV 2021)
Virtual Event
Feng, L.; Fisman, D.
978-3-030-88493-2
978-3-030-88494-9
Cimatti, Alessandro; Tian, Chun; Tonetta, Stefano
Assumption-Based Runtime Verification of Infinite-State Systems / Cimatti, Alessandro; Tian, Chun; Tonetta, Stefano. - 12974:(2021), pp. 207-227. (Intervento presentato al convegno Runtime Verification 2021 tenutosi a Virtual Event nel 11/10/2021) [10.1007/978-3-030-88494-9_11].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/319729
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 3
social impact