Case Study: Modeling, Simulation, Verification, and Code Generation of an Automatic Cruise Control System

Cyber-Physical Systems (CPSs) seamlessly integrate computational and physical capabilities, that expand the capabilities of physical world through communication, computation, and control. As pointed out by Jones, any failure of these systems may cause severe catastrophes, especially for safety-critical applications. The Model Based Design (MBD) approach can control complexity of systems by appropriate abstraction/refinement and composition/decomposition, and meanwhile provides techniques based on modeling, analysis, and verification in order to detect and correct errors in the early stage of design. However, the MBD for CPSs faces challenges, for it is difficult to consider all the three aspects, including physical processes, software functionality, and system architecture, uniformly in CPS design. To address this issue, we proposed a unified graphical framework combing AADL and Simulink/Stateflow, called \(\textsf {AADL}\!\oplus \!\textsf {S/S}\) , for modeling all the three aspects of CPSs, and we also presented the translation from informal \(\textsf {AADL}\!\oplus \!\textsf {S/S}\) to formal Hybrid Communicating Sequential Processes (HCSP) and finally to C code. In this paper, we introduce a case study of a realistically-scaled automatic cruise control system. The goal of this case study is to show the whole procedure of modeling, simulation, verification, and code generation of the MBD methodology, illustrate the combined framework of AADL and Simulink/Stateflow to cover all the three aspects of CPS design, as well as the capability of analyzing the combined model, and finally demonstrate the practicability of our MBD approach for complex CPSs.