Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
We survey some of the problems associated with checking whether a given behavior (a sequence, a Boolean signal or a continuous signal) satisfies a property specified in an appropriate temporal logic and describe two such monitoring algorithms for the real
- PDF / 802,366 Bytes
- 31 Pages / 430 x 660 pts Page_size
- 58 Downloads / 158 Views
3
Verimag, 2 Av. de Vignate, 38610 Gi`eres, France [email protected], [email protected] 2 Weizmann Institute of Science, Rehovot 76100, Israel New York University, 251 Mercer St. New York, NY 10012, USA [email protected] Words, even infinite words, have their limits. Dedicated to B.A. Trakhtenbrot on his 85th Birthday.
Abstract. We survey some of the problems associated with checking whether a given behavior (a sequence, a Boolean signal or a continuous signal) satisfies a property specified in an appropriate temporal logic and describe two such monitoring algorithms for the real-time logic MITL.
1
Introduction
This paper is concerned with the following problem: Given a temporal property ϕ how does one check that a given behavior ξ satisfies it. Within this paper we assume that the behavior to be checked is produced by a model of a dynamical system S, although some of the techniques are applicable to behaviors generated by real physical systems. Unlike formal verification which aims at showing that all behaviors generated by S satisfy ϕ, here S is used to generate one behavior at a time and can thus be viewed as a black box. This setting has been studied extensively in recent years both in the context of digital hardware, under the names of “dynamic” verification, or assertion checking as well as for software, where it is referred to as runtime verification [15,39]. We will use the term monitoring. In this framework the question of coverage, that is, finding a finite number of test cases whose behavior will guarantee overall correctness, is delegated outside the scope of the property monitor. This approach can be used when the system model is too large to be verified formally. It is also applicable when the “model” in question is nothing but a hardly-formalizable simulation program, as is often the case in electrical simulation of circuits. On the other hand, the explicit presentation of ξ itself, rather than using the generating model S, raises new problems. Most of the work described in this paper has been performed within the European project PROSYD1 with the purpose of extending some ingredients 1
IST-2003-507219 PROSYD (Property-Based System Design).
A. Avron et al. (Eds.): Trakhtenbrot/Festschrift, LNCS 4800, pp. 475–505, 2008. c Springer-Verlag Berlin Heidelberg 2008
476
O. Maler, D. Nickovic, and A. Pnueli
of verification methodology from digital (discrete) to analog (continuous and hybrid) systems. Consequently, we treat systems and behaviors described at three different levels of abstraction (discrete, timed and continuous). Hence we find it useful to start with a generic model of a dynamical system defined over an abstract state space which evolves in an abstract time domain, see also [28,29]. The three models used in the paper are obtained as special instances of this model. States and Behaviors. A model S of a system is defined over a set V = {x1 , . . . xn } of state variables, each ranging over a domain Xi . The state space of the system is thus X = X1 × · · · × Xn . The system evolves over
Data Loading...
