A Rewriting Framework for Cyber-Physical Systems

The analysis of cyber-physical systems (CPS) is challenging due to the large state space and the continuous changes occurring in its parts. Design practices favor modularity to help reducing the complexity. In a previous work, we proposed a discrete semantic model for CPS that captures both cyber and physical aspects as streams of discrete observations, which ultimately form the behavior of a component. This semantic model is denotational and compositional, where each composition operator algebraically models the interaction between a pair of components. In this paper, we propose a specification of some components as rewrite systems. The specification is operational and executable, and we study conditions for its semantics as components to be compositional. We demonstrate our framework on modeling a coordination of robots moving on a shared field. We show that the system of robots can be coordinated by a protocol in order to exhibit emerging behavior. We use an implementation of our framework in Maude to give some practical results.