Circus
From MaRDI portal
swMATH21828MaRDI QIDQ33628FDOQ33628
Author name not available (Why is that?)
Official website: https://link.springer.com/chapter/10.1007/3-540-45648-1_10
Cited In (only showing first 100 items - show all)
- Title not available (Why is that?)
- A CSP model of Eiffel's SCOOP
- Responsiveness and stable revivals
- A denotational semantics for Handel-C
- A semantics for behavior trees using CSP with specification commands
- Cameo: an alternative model of concurrency for Eiffel
- Interface theories for concurrency and data
- Angelic nondeterminism in the unifying theories of programming
- Title not available (Why is that?)
- FeatherTrait
- Experiments in program verification using Event-B
- Mechanised support for sound refinement tactics
- Connectors as designs: modeling, refinement and test case generation
- Mechanical reasoning about families of UTP theories
- Refinement-oriented models of Stateflow charts
- FM 2005: Formal Methods
- From control law diagrams to Ada via \textsf{Circus}
- A refinement strategy for Circus
- Building program construction and verification tools from algebraic principles
- A UTP semantics for \textsf{Circus}
- Derivation of concurrent programs by stepwise scheduling of Event-B models
- On integrating confidentiality and functionality in a formal method
- Refinement patterns for ASTDs
- Denotational semantics and its algebraic derivation for an event-driven system-level language
- CCSP
- Simulink
- JACK
- StateFlow
- CZT
- ArcAngelC
- ClawZ
- ProofPower
- ProB
- Rodin
- A Hoare logic for linear systems
- csp2B
- Alcoa
- MIO Workbench
- Z/EVES
- Z
- CSP-prover
- FDR2
- Handel-C
- FDR3
- CSPsim
- PAT
- PTSC
- Verilog
- Isabelle/Circus
- ProBE
- NAT2TEST
- HOL-TestGen
- Encoding Circus programs in ProofPower-Z
- Automating refinement of Circus programs
- FM 2005: Formal Methods
- Integrating a formal method into a software engineering process with UML and Java
- Jaza
- Isabelle/UTP
- RailCNL
- Hume
- ZRC
- UTPCalc
- JCSP
- Simpl
- Connectors as designs
- A tactic language for refinement of state-rich concurrent specifications
- Semantic domains for Handel-C
- The behavioural semantics of Event-B refinement
- Test selection for traces refinement
- rCOS: a refinement calculus of object systems
- Testing for refinement in \textsf{Circus}
- A process algebraic framework for specification and validation of real-time systems
- A formal framework for modeling and validating simulink diagrams
- CSP with Hierarchical State
- The safety-critical Java memory model formalised
- Type checking \textsf{Circus} specifications
- A timeband framework for modelling real-time systems
- RiskStructures: a design algebra for risk-aware machines
- TraitCbC
- Testing using CSP Models: Time, Inputs, and Outputs
- Stateflow diagrams in Circus
- Laws of mission-based programming
- Building a Modal Interface Theory for Concurrency and Data
- A Unary Semigroup Trace Algebra
- rCOS: defining meanings of component-based software architectures
- Unifying theories of reactive design contracts
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
- A two-way path between formal and informal design of embedded systems
- Circus Time with Reactive Designs
- Refinement and verification in component-based model-driven design
- Modelling temporal behaviour in complex systems with Timebands
- Simulink timed models for program verification
- Behavioural models for FMI co-simulations
- SafeJML
- Refinement of actions in Circus
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
- Model transformations across views
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
- A stepwise approach to linking theories
- Efficient symbolic computation of process expressions
This page was built for software: Circus