Checking Finite Traces Using Alternating Automata |
| |
Authors: | Bernd Finkbeiner Henny Sipma |
| |
Affiliation: | (1) Computer Science Department, Stanford University, Stanford, CA 94305, USA |
| |
Abstract: | Alternating automata have been commonly used as a basis for static verification of reactive systems. In this paper we show how alternating automata can be used in runtime verification. We present three algorithms to check at runtime whether a reactive program satisfies a temporal specification, expressed by a linear-time temporal logic formula. The three methods start from the same alternating automaton but traverse the automaton in different ways: depth-first, breadth-first, and backwards, respectively. We then show how an extension of these algorithms, that collects statistical data while verifying the execution trace, can be used for a more detailed analysis of the runtime behavior. All three methods have been implemented and experimental results are presented. |
| |
Keywords: | runtime verification alternating automata trace checking temporal logic online monitoring |
本文献已被 SpringerLink 等数据库收录! |
|