Summary of An Algebra for Interaction of Cyber-Physical Components
Modelling 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 decisions 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 interaction occurring 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 behaviour.
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.
See: agenda item on the website of Leiden University
