RSS Meetups are monthly gatherings of LASIGE members with research interests mainly in Software Architecture, Verification, Testing, Programming Languages, Type Systems, Logic, Concurrency, and Formal Methods.
Abstract: 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 [1], 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 recent work, we proposed a specification of 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 use an implementation of our framework in Maude to analyze how a group of robots can be coordinated by a protocol in order to exhibit emerging behavior.