Specification, synthesis and validation of strategies for collaborative embedded systems

A collaborative embedded system is an autonomous component of a cyber-physical system which cooperates with other such systems in order to accomplish a common goal. In this paper, we report on approaches for the validation of such collaborative embedded systems. We describe specification methods for hierarchies of goals and targets. Using model checking of alternating signal temporal logic, we show how to construct strategies for the satisfaction of goals and targets. For runtime validation of safety properties, we give a robust monitoring procedure which can flag potential problems in advance. Our two examples are car platooning and automated guided vehicles in industrial production. In the car platooning example, autonomous vehicles collaborate to enable high-speed driving at short distances. The fleet of transport robots collaborates in loading and unloading of production machines.