From control law diagrams to Ada via \textsf{Circus}

DOI10.1007/s00165-010-0170-3zbMath1226.68028OpenAlexW2080864228MaRDI QIDQ640296

Colin O'Halloran, Phil Clayton, Ana Cavalcanti

Publication date: 18 October 2011

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-010-0170-3

zbMATH Keywords

CSPrefinementsimulink

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Testing using CSP Models: Time, Inputs, and Outputs ⋮ Behavioural Models for FMI Co-simulations ⋮ Refinement-oriented models of Stateflow charts ⋮ Safety-critical Java programs from \textsf{Circus} models ⋮ Test selection for traces refinement ⋮ Automated verification of reactive and concurrent programs by calculation ⋮ Towards Algebraic Semantics of Circus Time ⋮ Simulink Timed Models for Program Verification ⋮ Laws of mission-based programming

Uses Software

• ArcAngel
• Simulink
• ProofPower
• ClawZ
• Z
• ZRC
• Circus
• Hume

Cites Work

• ArcAngel: a tactic language for refinement
• A refinement strategy for Circus
• 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
• ZRC -- A refinement calculus for \(Z\)
• Stepwise Development of Simulink Models Using the Refinement Calculus Framework
• Automated Technology for Verification and Analysis
• Theoretical Aspects of Computing - ICTAC 2004
• FM 2005: Formal Methods
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item