A clock-based framework for construction of hybrid systems

Hybrid systems are composed by continuous physical component and discrete control component where the system state evolves over time according to interacting law of discrete and continuous dynamics. Combinations of computation and control can lead to very complicated system designs. Rather than address the formal verification of hybrid systems, this paper forcuses on general modelers, aimed at modelling hybrid dynamics in such a way one can extract the specification of the control component from the specification of the total system and the desire behaviour of the physical component. We treat more explicit hybrid models by providing a mathematical framework based on clock and synchronous signal. This paper presents an abstract concept of clock with two suitable metric spaces for description of temporal order and time latency, and links clocks with synchronous events by showing how to represent the occurrences of an event by a clock. We tackle discrete variables by giving them a clock-based representation, and show how to capture dynamical behaviours of continuous components by recording the time instants when a specific type of changes take place. This paper introduces a clock-based hybrid language for description and reasoning of both discrete and continuous dynamics, and applies it to a family of physical devices, and demonstrates how to specify a water tanker and construct and verify its controller based on clocks.