A denotational semantics of simulink with higher-order UTP

DOI10.1016/J.JLAMP.2022.100809MaRDI QIDQ2096416zbMATH OpenOpenAlexWikidataFDO

Authors Xiong Xu, Bohua Zhan, Jean-Pierre Talpin, Naijun Zhan, Shu-Ling Wang

Publication date 16 November 2022

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2022.100809

zbMATH Keywords

cyber-physical systemsdenotational semanticsmathworks simulinkmodel-based designunifying theory of programming

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• A contract-based semantics and refinement for Simulink
• Towards a UTP semantics for Modelica
• Compositional assume-guarantee reasoning of control law diagrams using UTP
• Formal verification of Simulink/Stateflow diagrams
• Simulink timed models for program verification

Cites work

• A lattice-theoretical fixpoint theorem and its applications
• Compositional assume-guarantee reasoning of control law diagrams using UTP
• Differential dynamic logic for hybrid systems
• Formal Verification of Simulink/Stateflow Diagrams
• Formal verification of Simulink/Stateflow diagrams
• Hybrid Systems: Computation and Control
• Mechanically proving determinacy of hierarchical block diagram translations
• Non-standard semantics of hybrid systems modelers
• Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations
• Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and simulink/stateflow
• Unifying theories of reactive design contracts
• Zélus: a synchronous language with ODEs

Cited in

(5)

• Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and simulink/stateflow
• Unified graphical co-modelling of cyber-physical systems using AADL and Simulink/Stateflow
• A contract-based semantics and refinement for Simulink
• \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
• A Coq implementation of the program algebra in Jifeng He's new roadmap for linking theories of programming

Describes a project that uses

Uses Software

• Simulink
• Zelus
• SL2SX
• Matlab

This page was built for publication: A denotational semantics of simulink with higher-order UTP

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