Formal Specification of Cyber Physical Systems: Three Case Studies Based on Clock Theory

Cyber Physical Systems are in charge of the control of physical processes characterized by their own dynamics. This control must comply with timing constraints - sometimes stringent ones-imposed by the Cyber Physical Systems. It is crucial to address these timing issues as early as possible in the development process to detect inconsistencies in the requirements or in the constraints and to capture changes in the system. This paper aims to apply the clock theory to the specification of Cyber Physical Systems. To illustrate the concept we develop three well-known case studies: the Steam Boiler Control System, Press and Railway Cross System.