The Design of Intelligent Temperature Control System of Smart House with MARS
摘要
MARS is a toolchain, supporting model-based design of cyber-physical systems (CPS), which integrates informal and formal design. With MARS, a system under development can be graphically modeled by the combination of AADL and Simulink/Stateflow, then the simulation of the graphical model can be conducted. Furthermore, the graphical model can be automatically transformed to Hybrid Communicating Sequential Processes (HCSP) for formal verification with HHLProver. Finally, ANSI-C code or SystemC code can be generated from the verified HCSP formal model with the guarantee of correctness. As a case study of CPS, in this paper, we apply MARS to design an intelligent temperature control system, including its modeling, simulation, verification and code generation. This case study demonstrates the advantages of the design of CPS with MARS, including the integration of modeling, simulation, verification and code generation; the integration of informal and formal design, thus providing balance between efficiency and rigidity.