Abstract
Hybrid automata combine finite state models with continuous variables that are governed by differential equations. Hybrid automata are used to model systems in a wide range of domains such as automotive control, robotics, electronic circuits, systems biology, and health care. Numerical simulation approximates the evolution of the variables with a sequence of points in discretized time. This highly scalable technique is widely used in engineering and design, but it is difficult to simulate all representative behaviors of a system. To ensure that no critical behaviors are missed, reachability analysis aims at accurately and quickly computing a cover of the states of the system that are reachable from a given set of initial states. Reachability can be used to formally show safety and bounded liveness properties. This chapter outlines the major concepts and discusses advantages and shortcomings of the different techniques.
| Original language | English |
|---|---|
| Title of host publication | Formal Modeling and Verification of Cyber-Physical Systems |
| Subtitle of host publication | 1st International Summer School on Methods and Tools for the Design of Digital Systems, Bremen, Germany, September 2015 |
| Publisher | Springer Fachmedien |
| Pages | 50-81 |
| Number of pages | 32 |
| ISBN (Electronic) | 9783658099947 |
| ISBN (Print) | 9783658099930 |
| DOIs | |
| Publication status | Published - 5 Jun 2015 |
| Externally published | Yes |