Formal Verification of Simulink/Stateflow Diagrams: A Deductive Approach

Formal Verification of Simulink/Stateflow Diagrams presents a state-of-the-art technique for formal verification of continuous-time Simulink and Stateflow diagrams, featuring: an expressive hybrid system modeling language, a powerful specification logic and deduction-based verification approach, and realistic case studies.  Readers learn the HCSP/HHL-based deductive method and the use of corresponding tools for formal verification of Simulink and Stateflow diagrams. They also gain basic knowledge about the fundamental elements of formal methods such as formal syntax and semantics, and especially the common techniques applied in formal modeling and verification of hybrid systems.

By investigating the successful case studies, readers realize how to apply the pure theory and techniques to real applications and develop their own formal methods in their future work.