Formal Verification of Simulink/Stateflow Diagrams

DOI10.1007/978-3-319-47016-0zbMath1412.68006OpenAlexW4234184051MaRDI QIDQ4600381

Naijun Zhan, Heng-Jun Zhao, Shu-Ling Wang

Publication date: 8 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-47016-0

zbMATH Keywords

embedded systemsmodel checkingHoare logiccontinuous-time systemsSimulinksystem verificationcommunicating processesunifying theories of programmingStateflowprogram invariant

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (6)

Characterizing positively invariant sets: inductive and topological methods ⋮ Synthesizing SystemC Code from Delay Hybrid CSP ⋮ \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic ⋮ Automated verification of reactive and concurrent programs by calculation ⋮ Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and simulink/stateflow ⋮ A denotational semantics of simulink with higher-order UTP

Uses Software

• Isabelle
• Simulink
• StateFlow

This page was built for publication: Formal Verification of Simulink/Stateflow Diagrams