A contract-based semantics and refinement for Simulink

DOI10.1007/978-3-031-21213-0_9MaRDI QIDQ6168983zbMATH OpenFDO

Authors Quan Sun, Wei Zhang, Chao Wang, Zhiming Liu

Publication date 10 August 2023

Published in Dependable Software Engineering. Theories, Tools, and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-21213-0_9

zbMATH Keywords

refinementcompositional reasoningSimulinkcontract-based semantics

Mathematics Subject Classification ID

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) Semantics in the theory of computing (68Q55) Mathematical modeling or simulation for problems pertaining to systems and control theory (93-10)

Recommendations

• Refinement-oriented models of Stateflow charts
• A denotational semantics of simulink with higher-order UTP
• Compositional assume-guarantee reasoning of control law diagrams using UTP
• Simulink timed models for program verification
• Stepwise Development of Simulink Models Using the Refinement Calculus Framework

Cites work

• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• A formal framework for modeling and validating simulink diagrams
• Compositional assume-guarantee reasoning of control law diagrams using UTP
• Contract-based verification of MATLAB-style matrix programs
• FM 2005: Formal Methods
• Graphical Modeling of Hybrid Dynamics with Simulink and Stateflow
• Semantic translation of Simulink diagrams to input/output extended finite automata
• Simulink timed models for program verification
• Stepwise Development of Simulink Models Using the Refinement Calculus Framework
• Taming Dr. Frankenstein: contract-based design for cyber-physical systems
• Unifying theories of reactive design contracts

This page was built for publication: A contract-based semantics and refinement for Simulink

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