Formal Verification of Simulink/Stateflow Diagrams

DOI10.1007/978-3-319-24953-7_33zbMath1471.68159OpenAlexW4379506493MaRDI QIDQ3460585

Martin Fränzle, Liang Zou, Naijun Zhan, 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 verificationSimulink/Stateflowhybrid CSPhybrid Hoare logic

Mathematics Subject Classification ID

Application models in control theory (93C95) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30) 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)

Related Items (8)

Continuity as a computational effect ⋮ Reachability analysis and simulation for hybridised Event-B models ⋮ Reusable contracts for safe integration of reinforcement learning in hybrid systems ⋮ \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic ⋮ Towards a UTP Semantics for Modelica ⋮ A Two-Way Path Between Formal and Informal Design of Embedded Systems ⋮ 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/HOL
• Simulink
• StateFlow

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