Simulink timed models for program verification

DOI10.1007/978-3-642-39698-4_6MaRDI QIDQ2842628zbMATH OpenOpenAlexFDO

Authors Ana Cavalcanti, Alexandre Mota, Jim Woodcock

Publication date 16 August 2013

Published in Theories of Programming and Formal Methods (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-39698-4_6

zbMATH Keywords

modellingCSPtimerefinementZCircusSimulink

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A formal framework for modeling and validating simulink diagrams
• From control law diagrams to Ada via \textsf{Circus}
• Refinement-oriented models of Stateflow charts
• Formal verification of Simulink/Stateflow diagrams
• Stateflow diagrams in Circus

Cites work

• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• scientific article; zbMATH DE number 1949640 (Why is no real title available?)
• scientific article; zbMATH DE number 2017341 (Why is no real title available?)
• scientific article; zbMATH DE number 2080001 (Why is no real title available?)
• A UTP semantics for \textsf{Circus}
• A formal framework for modeling and validating simulink diagrams
• A process algebraic framework for specification and validation of real-time systems
• A timed model for communicating sequential processes
• Angelic nondeterminism in the unifying theories of programming
• FM 2005: Formal Methods
• From control law diagrams to Ada via \textsf{Circus}
• Model-checking CSP-Z: Strategy, tool support and industrial application
• Stepwise Development of Simulink Models Using the Refinement Calculus Framework
• Theoretical Aspects of Computing - ICTAC 2004
• Unifying theories in ProofPower-Z

Cited in

(9)

• The refinement calculus of reactive systems
• Refinement-oriented models of Stateflow charts
• Angelic processes for CSP via the UTP
• FM 2005: Formal Methods
• A contract-based semantics and refinement for Simulink
• Behavioural models for FMI co-simulations
• On checking equivalence of simulation scripts
• A formal framework for modeling and validating simulink diagrams
• Compositional assume-guarantee reasoning of control law diagrams using UTP

Describes a project that uses

Uses Software

• Archive Formal Proofs
• Circus
• Isabelle/Circus
• Z
• ClawZ
• ProofPower
• Simulink

This page was built for publication: Simulink timed models for program verification

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