Simulink Timed Models for Program Verification

DOI10.1007/978-3-642-39698-4_6zbMath1390.68423OpenAlexW126787391MaRDI QIDQ2842628

Alexandre Mota, Ana Cavalcanti, J. C. P. 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

modellingZCSPrefinementtimeSimulinkCircus

Mathematics Subject Classification ID

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

Related Items (4)

The refinement calculus of reactive systems ⋮ A contract-based semantics and refinement for Simulink ⋮ Angelic processes for CSP via the UTP ⋮ Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• From control law diagrams to Ada via \textsf{Circus}
• Angelic nondeterminism in the unifying theories of programming
• A process algebraic framework for specification and validation of real-time systems
• A UTP semantics for \textsf{Circus}
• A formal framework for modeling and validating simulink diagrams
• A timed model for communicating sequential processes
• Unifying theories in ProofPower-Z
• Stepwise Development of Simulink Models Using the Refinement Calculus Framework
• Theoretical Aspects of Computing - ICTAC 2004
• FM 2005: Formal Methods
• Model-checking CSP-Z: Strategy, tool support and industrial application

This page was built for publication: Simulink Timed Models for Program Verification