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

DOI10.1007/S00165-010-0170-3zbMATH Open1226.68028OpenAlexW2080864228MaRDI QIDQ640296FDOQ640296

Authors Ana Cavalcanti, Phil Clayton, Colin O'Halloran 

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)

Recommendations

• scientific article; zbMATH DE number 2085322
• FM 2005: Formal Methods
• A Common Framework for Automata Theory and Control Theory
• A compositional framework for controller synthesis
• Axioms for control operators in the CPS hierarchy
• scientific article; zbMATH DE number 2084913
• Logic control and ``reactive systems: algorithmization and programming

Cites Work

• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• 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 1031982 (Why is no real title available?)
• scientific article; zbMATH DE number 1956625 (Why is no real title available?)
• scientific article; zbMATH DE number 1982196 (Why is no real title available?)
• scientific article; zbMATH DE number 2017341 (Why is no real title available?)
• scientific article; zbMATH DE number 2080012 (Why is no real title available?)
• scientific article; zbMATH DE number 1487746 (Why is no real title available?)
• scientific article; zbMATH DE number 1519981 (Why is no real title available?)
• scientific article; zbMATH DE number 2085344 (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 refinement strategy for Circus
• ArcAngel: a tactic language for refinement
• Automated Technology for Verification and Analysis
• FM 2005: Formal Methods
• Stepwise Development of Simulink Models Using the Refinement Calculus Framework
• Theoretical Aspects of Computing - ICTAC 2004
• ZRC -- A refinement calculus for \(Z\)

Cited In (12)

• Testing using CSP Models: Time, Inputs, and Outputs
• Stateflow diagrams in Circus
• Laws of mission-based programming
• Refinement-oriented models of Stateflow charts
• FM 2005: Formal Methods
• Simulink timed models for program verification
• Behavioural models for FMI co-simulations
• Towards Algebraic Semantics of Circus Time
• Test selection for traces refinement
• Safety-critical Java programs from \textsf{Circus} models
• Compositional assume-guarantee reasoning of control law diagrams using UTP
• Automated verification of reactive and concurrent programs by calculation

Uses Software

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

This page was built for publication: From control law diagrams to Ada via \textsf{Circus}

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