Towards Focus on Time

spichkov/Institut fur Informatik, TU M¨ unchen,¨Boltzmannstr. 3, 85748 Garching, GermanyAbstract: On specifying and verifying timing system properties in a formal way.Keywords: Formal Methods, Specification, Verification, Real-Time SystemsSpecifying real-time systems, arguing about timing properties is hardly avoidable. The notionof time takes center stage for this kind of systems: abstracting from the time we may loose thecore properties of a system we represent, e.g. in many cases the causality property can be loosed.In particular, the timed domain is the most important one for representation of distributed systemswith real-time requirements.On the other hand, in many cases arguing about time makes the specification more readablefor an average engineer: specification of a real-time system in an untimed frame may be in somecases shorter or more elegant from mathematical point of view, but to understand such specifica-tions and to argue about their properties is in many cases much more difficult in comparison tothe corresponding specifications in a timed frame, where some properties like causality could berepresented explicitly. Moreover, abstraction from timing aspects can easily lead to specificationmistakes because of difficulties to find a correct abstraction.One of the most well-established models for the specification and verification of real-timesystem design is representation of a system using timed automata, introduced by Alur andDill [AD94] – them extend the classical finite automata by a finite set of real valued clocksused to measure the time elapsed between events to constrain the runs of the automation. Themodel from Alur and Dill is well-developed, however, some its assumptions on the system couldbe too idealistic: timed automata assumes perfect continuity of clocks and, what could be evenmore critical if we deal with embedded systems, instantaneous reaction times. Another problemof this model is that it does not prevent Zeno runs [GB07]. To solve this, the idea of robust modelchecking was introduced by Puri [Pur00] and also revised in other approaches.We suggest another solution: to argue not about a single action or messages but about timeintervals containing a finite number of actions, i.e. to argue not about single messages in aninput stream, but about a sequence of messages that are present in this stream at some timeinterval. This sequence can be in general either empty or contain a single message or a numberof messages. In this approach a discrete model of time is used, because (i) this simplifies thespecification and, even more, the verification of system properties, and (ii) any timed transitionsystem can be discretized without loss of generality. Thus, an input for our timed automata or,more generally, a timed component, is an infinite sequence of finite time intervals.However a discrete model of time is used here, ones can choose any time granularity definingthe concrete meaning of a time interval according to the system requirements, and, moreover,it is possible to switch from one time granularity to another: the operator s ’