Formal verification of Simulink/Stateflow diagrams

DOI10.1007/978-3-319-24953-7_33MaRDI QIDQ3460585zbMATH OpenOpenAlexFDO

Authors Liang Zou, Naijun Zhan, Martin Fränzle, Shu-Ling Wang

Publication date 8 January 2016

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-24953-7_33

zbMATH Keywords

formal verificationhybrid CSPhybrid Hoare logicSimulink/Stateflow

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Mathematical modeling or simulation for problems pertaining to systems and control theory (93-10) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30) Application models in control theory (93C95)

Recommendations

• Formal Verification of Simulink/Stateflow Diagrams
• Refinement-oriented models of Stateflow charts
• Compositional assume-guarantee reasoning of control law diagrams using UTP
• Automated analysis of Stateflow models
• A formal framework for modeling and validating simulink diagrams

Cited in

(23)

• A formal framework for modeling and validating simulink diagrams
• 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
• Reachability analysis and simulation for hybridised Event-B models
• Mechanically proving determinacy of hierarchical block diagram translations
• Continuity as a computational effect
• Simulink timed models for program verification
• Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations
• Towards a UTP semantics for Modelica
• A two-way path between formal and informal design of embedded systems
• Dynamic state machines for formalizing railway control system specifications
• An instrumentation-based approach to controller validation
• Semantic translation of Simulink diagrams to input/output extended finite automata
• Refinement-oriented models of Stateflow charts
• Localizing Faults in Simulink/Stateflow Models with STL
• SyLVaaS: system level formal verification as a service
• Formal Verification of Simulink/Stateflow Diagrams
• Automated analysis of Stateflow models
• Stateflow diagrams in Circus
• Compositional assume-guarantee reasoning of control law diagrams using UTP
• Reusable contracts for safe integration of reinforcement learning in hybrid systems
• \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
• Embedding differential dynamic logic in PVS

Describes a project that uses

Uses Software

• Isabelle/HOL
• StateFlow
• Simulink

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 Q3460585)