Formal Verification of Simulink/Stateflow Diagrams

1. Introduction
Naijun Zhan, Shuling Wang, Hengjun Zhao

2. Preliminaries
Naijun Zhan, Shuling Wang, Hengjun Zhao

3. Unifying Theories of Programming (UTP)
Naijun Zhan, Shuling Wang, Hengjun Zhao

4. Simulink
Naijun Zhan, Shuling Wang, Hengjun Zhao

5. Stateflow and Its Combination with Simulink
Naijun Zhan, Shuling Wang, Hengjun Zhao

6. Hybrid CSP
Naijun Zhan, Shuling Wang, Hengjun Zhao

7. Hybrid Hoare Logic
Naijun Zhan, Shuling Wang, Hengjun Zhao

8. The HHL Prover
Naijun Zhan, Shuling Wang, Hengjun Zhao

9. Invariant Generation
Naijun Zhan, Shuling Wang, Hengjun Zhao

10. Translating Simulink Diagrams into HCSP
Naijun Zhan, Shuling Wang, Hengjun Zhao

11. Translating Simulink/Stateflow Diagrams into HCSP
Naijun Zhan, Shuling Wang, Hengjun Zhao

12. From HCSP to Simulink
Naijun Zhan, Shuling Wang, Hengjun Zhao

13. MARS: A Toolkit for Modelling, Analysis, and Verification of Hybrid Systems
Naijun Zhan, Shuling Wang, Hengjun Zhao

14. Case Studies
Naijun Zhan, Shuling Wang, Hengjun Zhao

Keywords: Engineering, Circuits and Systems, Processor Architectures, Electronic Circuits and Devices