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.
CITATION STYLE
Platzer, A. (2018). Safety & Contracts. In Logical Foundations of Cyber-Physical Systems (pp. 95–136). Springer International Publishing. https://doi.org/10.1007/978-3-319-63588-0_4
Mendeley helps you to discover research relevant for your work.