An algebra for interaction of cyber-physical components

Modeling and analysis of cyber-physical systems are still challenging. One reason is that cyber-physical systems involve many different parts (cyber or physical), of different nature (discrete or continuous), and in constant interaction via sensing and actuating.For instance, consider a group of robots, each running a program that takes decision based on the sequence of sensor readings. The sensors that equip a robot return the current position of the robot and the position of any adjacent obstacle. The interactionoccurring between each robot in the group cannot be derived solely from the specification of individual robots. If the field on which the robots roam changes its property, the same group of robots might sense different values, and therefore take different actions. Also, the time at which a robot acts and senses will affect the decision of each controller and will change the resulting collective behavior.This thesis proposes a compositional approach to the design and programming of interacting cyber-physical components. We present an algebra that provides a novel perspective on modeling interaction of cyber-physical components. Using our algebraic framework, one can design a complex cyber-physical system by first designing each part, and then specifying how the parts interact. We formalized the relation between our abstract semantic model and an implementation written in Maude, a programming language based on rewriting logic. We present some applications, including safety and liveness properties of a system consisting of a set of robots, each equipped with a battery, running on a shared field.