Prof. Dr. Holger Giese


Talk 'Towards Verifying CPS with Structural Dynamism' of Prof. Giese together with Basil Becker


In our work we focus on distributed, decentralizand safety-critical cyber-physical systems where the combination of networking and control results in new opportunities. We especially emphasize systems which face inherent complex structural dynamism due to such phenomena as mechanical coupling of moving parts, mobility and coalition building or self-organization. Thus, a technique that aims at verifying such systems first has to cope with the complexity introduced by the system's physical nature and second has to be able to cope with complex structural changes that also impact the physical behavior. For our approach we employ graph transformation systems with continuous behavior in form of ODE to capture the behavior of such CPS. Furthermore, we extended our invariant checking technique -- a technique that can statically verify inductive invariants for sets of timed graph transformation rules and timed graph constraints -- to also deal with differential equations for the continuous behavior. We exemplify our approach using a system of autonomous shuttles. For these shuttles we want to verify that platooning is safe and no collision occur. Obviously in a real-world system a tremendous number of situations exist where a collision could happen. We use graph transformation rules to describe the shuttles abstract movement on the topology and the creation of a platoon and graph pattern to describe collisions that have to be excluded. Continuous attributes, whose derivation is given through ODE, together with attribute constraints describe speed, acceleration and position.