Abstract

Recently we propose an approach to designing embedded real-time systems formally. Using our approach, one can first build a graphical model of a system to be developed with Simulink/Stateflow (S/S), and then conduct extensive simulation. In order to verify the graphical model formally, we translate S/S diagrams into HCSP automatically. HCSP is a formal modeling language for hybrid systems, an extension of CSP by introducing differential equations to model continuous evolution and several kinds of interrupts to model the interaction between continuous evolution and discrete jumps. Using Hybrid Hoare Logic and its theorem prover, the translated HCSP model can be verified. For justifying the correctness of the translation, we give an inverse translation from HCSP to Simulink, so that the consistency can be checked by co-simulation. By providing a set of refinement rules, an HCSP process can be generated into a piece of SystemC code, approximate bisimilar to the original HCSP process. All work can be supported by a developed tool MARS. Several real-world case studies have been investigated to check the feasibility of the approach.