Cyber-Physical Systems

Chapter 6. Logical Correctness for Hybrid Systems

Sagar Chaki, Edmund Clarke, Arie Gurfinkel, and John Hudak

A hybrid system is a dynamic system whose behavior changes both discretely and continuously. Hybrid systems constitute a powerful formalism for understanding, modeling, and reasoning about a wide range of devices that affect our day-to-day lives. These range from the simple, such as a room thermostat, to the critical, such as the airbag controller in a vehicle. Hybrid systems also enable rigorous analysis to be performed that can verify and predict correct behavior of such devices. In this chapter, we discuss different types of functional correctness problems that arise in the context of hybrid systems. For each category, we present sample ...