Title
Monitoring First-Order Interval Logic
Abstract
Runtime verification is used for monitoring the execution of systems, e.g. checking sequences of reported events against formal specifications. Typically the specification refers to the individual monitored events. In this work we perceive the events as defining intervals, each defined by a begin and a subsequent end event. Allen's logic allows assertions about the relationship between such named intervals. We suggest a formalism that extends Allen's logic into a first-order logic that allows quantification over intervals; in addition, intervals can carry data. We provide a monitoring algorithm and describe an implementation and experiments performed with it. We furthermore describe an alternative method for monitoring properties in this logic, by translating them into first-order past-time temporal logic, monitored with the tool DejaVu.
Year
DOI
Venue
2021
10.1007/978-3-030-92124-8_4
SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2021)
DocType
Volume
ISSN
Conference
13085
0302-9743
Citations 
PageRank 
References 
0
0.34
0
Authors
3
Name
Order
Citations
PageRank
Klaus Havelund100.34
Moran Omer200.34
Doron Peled33357273.18