ABSTRACT
CONTENTS 10.1 Introduction 238 10.2 Related Works 239 10.3 Preliminaries 241
10.3.1 ACC+ 241 10.3.2 Dierential Dynamic Logic (dL) 242 10.3.3 Verication Tool: KeYmaera 243
10.4 A High-Level Safety Concept Abstraction for ACC+ Systems 243 10.4.1 Verication 245 10.4.2 Controllability 247
10.5 Renement of the Safety Concept into a Practical ACC+ Model 248 10.5.1 Controller Modes 250 10.5.2 Mode Switching 253 10.5.3 Continuous Controller Design 258 10.5.4 Simulation Results 259 10.5.5 Verication 260 10.5.6 Safe Refactoring 263
10.6 Conclusion 268 References 268
Automotive cyber-physical systems (Auto-CPS) are safety critical systems inwhich failure can lead to grave consequences, such as nancial loss, severe injuries, or even loss of life. Auto-CPS consists of tightly coupled interactions of computational units and physical systems that involve interplay among embedded systems, control theory, realtime systems, and software engineering. Increases in software-related recalls of vehicles are driving demand for methods to cost-eectively produce safe, secure, and reliable cars with more than 100 electronic control units (ECUs) communicating over vehicle networks. Since formal methods have played a signicant role in developing safe and dependable systems, the role of formal methods in developing Auto-CPS should be taken into account. In this work, we will demonstrate the benets and limitations of formal methods for Auto-CPS by considering a relatively new driver assistance feature.
