Technische Universität München Robotics and Embedded Systems

Formal Verification of Cyber-Physical Systems



In many modern systems, computing elements are tightly connected with physical entities for which the term "cyber-physical systems" has been established in recent years. Cyber-physical systems fulfill tasks that are increasingly operational- and safety-critical. Examples are automated vehicles, surgical robots, smart grids, and collaborative human-robot manufacturing. The advanced capabilities of cyber-physical systems require complex software and control algorithms, which are hard to verify, i.e., to show that the system behaves as specified. A possible solution is to algorithmically prove the correctness of the system with respect to a formal specification. There exist already methods for the formal verification of discrete systems, however, cyber-physical systems have a hybrid dynamics in which discrete and continuous dynamics are interconnected.

Formal Verification of Cyber-Physical Systems


New methods are developed that formally verify systems with hybrid dynamics. Especially reachability analysis is used, which computes the set of all possible (infinitely many) solutions of a hybrid system for a set of initial states and a set of possible system inputs. If the reachable set does not intersect a set of unsafe states, one can formally show that no solution exists which violates the system. This approach has been applied to automated cars, smart grids, and automotive control.