Motivation
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.
Objective
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.
Development
Most of the methods developed for formal verification of cyber-physical systems are realized in the tool CORA.
