Circus

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