Towards the Modular Specification and Validation of Cyber-Physical Systems

Cyber-Physical Systems (CPS) are systems controlled by one or more computer-based components tightly integrated with a set of physical components, typically described as sensors and actuators, that can either be directly attached to the computer components, or at a remote location, and accessible through a network connection. The modeling and verification of such systems is a hard task and error prone that require rigorous techniques. Hybrid automata is a formalism that extends finite-state automata with continuous behavior, described by ordinary differential equations. This paper uses a rewriting logic-based technique to model and validate CPS, thus exploring the use of a formal technique to develop such systems that combines expressive specification with efficient state-based analysis. Moreover, we aim at the modular specification of such systems such that each CPS component is independently specified and the final system emerges as the synchronous product of its constituent components. We model CPSs using Linear Hybrid Automaton and implement them in Real-Time Maude, a rewriting logic tool for real-time systems. With this method, we develop a specification for the $n$-reservoir problem, a CPS that controls a hose to fill a number of reservoirs according to the physical properties of the hose and the reservoirs.