From control law diagrams to Ada via \textsf{Circus}
From MaRDI portal
Publication:640296
Recommendations
- Hybrid control loops, A/D maps, and dynamic specifications
- 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
- (Control, output) synthesis: Algebraic paradigms
- Logic control and ``reactive systems: algorithmization and programming
Cites work
- A formal framework for modeling and validating simulink diagrams
- A Giotto-based helicopter control system
- A Hoare logic for single-input single-output continuous-time control systems
- A process algebraic framework for specification and validation of real-time systems
- A refinement strategy for Circus
- A UTP semantics for \textsf{Circus}
- ArcAngel: a tactic language for refinement
- Automated Technology for Verification and Analysis
- FM 2005: Formal Methods
- Formal modeling and analysis of an avionics triplex sensor voter
- Generalised substitution language and differentials
- 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 1519981 (Why is no real title available?)
- Series of abstractions for hybrid automata
- Stepwise Development of Simulink Models Using the Refinement Calculus Framework
- Theoretical Aspects of Computing - ICTAC 2004
- Using a process algebra to control B OPERATIONS
- ZRC -- A refinement calculus for Z
Cited in
(12)- Automated verification of reactive and concurrent programs by calculation
- Laws of mission-based programming
- Safety-critical Java programs from \textsf{Circus} models
- Towards Algebraic Semantics of Circus Time
- Simulink timed models for program verification
- Behavioural models for FMI co-simulations
- Refinement-oriented models of Stateflow charts
- Test selection for traces refinement
- Stateflow diagrams in Circus
- FM 2005: Formal Methods
- Compositional assume-guarantee reasoning of control law diagrams using UTP
- Testing using CSP Models: Time, Inputs, and Outputs
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)
