From control law diagrams to Ada via \textsf{Circus}
From MaRDI portal
Publication:640296
DOI10.1007/S00165-010-0170-3zbMATH Open1226.68028OpenAlexW2080864228MaRDI QIDQ640296FDOQ640296
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
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
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- ArcAngel: a tactic language for refinement
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A UTP semantics for \textsf{Circus}
- ZRC -- A refinement calculus for \(Z\)
- FM 2005: Formal Methods
- A refinement strategy for Circus
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A formal framework for modeling and validating simulink diagrams
- Stepwise Development of Simulink Models Using the Refinement Calculus Framework
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automated Technology for Verification and Analysis
- Theoretical Aspects of Computing - ICTAC 2004
- A process algebraic framework for specification and validation of real-time systems
Cited In (10)
- Testing using CSP Models: Time, Inputs, and Outputs
- Laws of mission-based programming
- Refinement-oriented models of Stateflow charts
- FM 2005: Formal Methods
- Towards Algebraic Semantics of Circus Time
- Simulink Timed Models for Program Verification
- Test selection for traces refinement
- Behavioural Models for FMI Co-simulations
- Safety-critical Java programs from \textsf{Circus} models
- Automated verification of reactive and concurrent programs by calculation
Uses Software
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)
