Verification via digitized models of real-time hybrid systems

Abstract

The paper presents an approach to the specification and verification of real-time hybrid systems using duration calculus (DC). By introducing a formula int to DC to express the intervals of time between two ticks of the system clock, it is shown that DC can be used to specify both the digital states and the analog states as well as to reason about time in distributed systems. The authors illustrate their approach by giving an intuitive model for the communication protocols in which the verification can be done by using the familiar natural induction rules.