Safety & Contracts

Synopsis

This chapter provides a lightweight introduction to safety specification techniques for cyber-physical systems. It discusses how program contracts generalize to CPS by declaring expectations on the initial states together with guarantees for all possible final states of a CPS model. Since assumptions and guarantees can be quite subtle for CPS applications, it is important to capture them early during a CPS design. This chapter introduces differential dynamic logic, a logic for specifying and verifying hybrid systems, which provides a formal underpinning for the precise meaning of CPS contracts. In subsequent chapters, differential dynamic logic plays a central rôle in rigorous verification of CPSs as well. This chapter also develops the running example of Quantum the bouncing ball, which is a hopelessly impoverished CPS but still features many of the important dynamical aspects of CPS in a perfectly intuitive setting.