Towards the Modular Specification and Validation of Cyber-Physical Systems

TL;DR

This paper presents a modular, formal approach using rewriting logic and hybrid automata to model and verify cyber-physical systems, enabling independent component specification and efficient validation.

Contribution

It introduces a modular specification framework for CPS using Linear Hybrid Automata and Real-Time Maude, facilitating independent component modeling and system validation.

Findings

Successful modeling of the $n$-reservoir problem in Real-Time Maude.

Demonstrates modular CPS specification enables independent component analysis.

Validates the approach through formal verification of system properties.

Abstract

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.