From Timed to Hybrid Systems

We propose a framework for the formal speci cation and veri cation of timed and hybrid systems. For timed systems we propose a speci cation language that refers to time only through age functions which measure the length of the most recent time interval in which a given formula has been continuously true. We then consider hybrid systems, which are systems consisting of a non-trivial mixture of discrete and continuous components, such as a digital controller that controls a continuous environment. The proposed framework extends the temporal logic approach which has proven useful for the formal analysis of discrete systems such as reactive programs. The new framework consists of a semantic model for hybrid time, the notion of phase transition systems, which extends the formalism of discrete transition systems, an extended version of Statecharts for the speci cation of hybrid behaviors, and an extended version of temporal logic that enables reasoning about continuous change.

• Type: Conference
• Year: 1991
• Where: REX
• Authors: Oded Maler, Zohar Manna, Amir Pnueli
• Keywords: Distributed And Parallel Computing, Formal Speci Cation, Hybrid Systems, REX 1991, Speci Cation