Formal Verification of Simulink/Stateflow Diagrams

DOI10.1007/978-3-319-47016-0MaRDI QIDQ4600381zbMATH OpenOpenAlexFDO

Authors Naijun Zhan, Shu-Ling Wang, Hengjun Zhao

Publication date 8 January 2018

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

zbMATH Keywords

communicating processescontinuous-time systemsembedded systemsHoare logicmodel checkingprogram invariantSimulinkStateflowsystem verificationunifying theories of programming

Mathematics Subject Classification ID

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

Recommendations

• Formal verification of Simulink/Stateflow diagrams
• A formal framework for modeling and validating simulink diagrams
• scientific article; zbMATH DE number 1390247
• Simulator semantics for system level formal verification
• scientific article; zbMATH DE number 7730622
• Formal system verification. State-of the-art and future trends

Cited in

(17)

• A formal framework for modeling and validating simulink diagrams
• 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
• Characterizing positively invariant sets: inductive and topological methods
• Mechanically proving determinacy of hierarchical block diagram translations
• Formal analysis and verification of Statemate designs
• Contract-based verification of MATLAB-style matrix programs
• Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations
• A two-way path between formal and informal design of embedded systems
• Formal verification of Simulink/Stateflow diagrams
• Formal verification of control systems software
• Formal system verification. State-of the-art and future trends
• Automated analysis of Stateflow models
• Synthesizing SystemC Code from Delay Hybrid CSP
• Compositional assume-guarantee reasoning of control law diagrams using UTP
• \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic

Describes a project that uses

Uses Software

• StateFlow
• Simulink
• Isabelle

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4600381)