Hybrid systems play an increasingly important role in transportation networks, robotics and in fields such as medicine and biology. Today hybrid systems are found in sophisticated embedded controllers used in the airplane industry, but also in medical devices that monitor serious health conditions. As hybrid systems are often part of devices operating in safety-critical situations, the verification of their safety properties becomes increasingly important. A hybrid system is considered safe if it is not possible for the system during its evolution to enter an unsafe state starting from an initial safe state. This project develops modeling algorithms and analysis techniques for the verification of safety properties of hybrid systems. Its main goal is the design and implementation of a probabilistically complete framework for computing trajectories that take the system from a safe to an unsafe state, or witness trajectories. Existence of a witness trajectory indicates that the hybrid system is not safe. When a witness trajectory is not found, the repeated application of the proposed methodology can increase the user's confidence in the safety of the system. Since hybrid systems have discrete and continuous aspects of control, a witness trajectory consists of one or more continuous parts interleaved with discrete transitions. This project blends in a novel way search methods for continuous spaces inspired by research in robot motion planning, with search techniques for discrete spaces and formal tools. The problem addressed is of central importance for the creation of high-confidence hybrid and embedded systems with reliability guarantees.
