Circus

swMATH21828MaRDI QIDQ33628

No author found.

Related Items (75)

Testing using CSP Models: Time, Inputs, and Outputs ⋮ Building a Modal Interface Theory for Concurrency and Data ⋮ Unnamed Item ⋮ Circus Time with Reactive Designs ⋮ Cameo: an alternative model of concurrency for Eiffel ⋮ Behavioural Models for FMI Co-simulations ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ Building Specifications in the Event-B Institution ⋮ Angelic nondeterminism in the unifying theories of programming ⋮ rCOS: a refinement calculus of object systems ⋮ Responsiveness and stable revivals ⋮ Interactive tool support for CSP \(\parallel\) B consistency checking ⋮ Efficient symbolic computation of process expressions ⋮ A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency ⋮ rCOS: Defining Meanings of Component-Based Software Architectures ⋮ Unifying Theories of Programming in Isabelle ⋮ A Unary Semigroup Trace Algebra ⋮ The safety-critical Java memory model formalised ⋮ Unifying theories in ProofPower-Z ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ Categorical foundations for structured specifications in \(\mathsf{Z}\) ⋮ Denotational semantics and its algebraic derivation for an event-driven system-level language ⋮ Unnamed Item ⋮ Mechanised support for sound refinement tactics ⋮ Experiments in program verification using Event-B ⋮ Connectors as designs: modeling, refinement and test case generation ⋮ Mechanical reasoning about families of UTP theories ⋮ Refinement-oriented models of Stateflow charts ⋮ Towards a UTP Semantics for Modelica ⋮ A Two-Way Path Between Formal and Informal Design of Embedded Systems ⋮ A Stepwise Approach to Linking Theories ⋮ From control law diagrams to Ada via \textsf{Circus} ⋮ Unifying theories of time with generalised reactive processes ⋮ Safety-critical Java programs from \textsf{Circus} models ⋮ A Hoare logic for linear systems ⋮ Proving Quicksort Correct in Event-B ⋮ Test selection for traces refinement ⋮ Automating Refinement of Circus Programs ⋮ A CSP model of Eiffel's SCOOP ⋮ RiskStructures: a design algebra for risk-aware machines ⋮ FM 2005: Formal Methods ⋮ FM 2005: Formal Methods ⋮ Modelling temporal behaviour in complex systems with Timebands ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Integrating a formal method into a software engineering process with UML and Java ⋮ Unnamed Item ⋮ A denotational semantics for Handel-C ⋮ A process algebraic framework for specification and validation of real-time systems ⋮ A tactic language for refinement of state-rich concurrent specifications ⋮ Unifying theories of reactive design contracts ⋮ Encoding Circus Programs in ProofPowerZ ⋮ Interface theories for concurrency and data ⋮ A semantics for behavior trees using CSP with specification commands ⋮ Stateflow Diagrams in ⋮ Mechanical Reasoning about Families of UTP Theories ⋮ A refinement strategy for Circus ⋮ Model transformations across views ⋮ A timeband framework for modelling real-time systems ⋮ CSP with Hierarchical State ⋮ A UTP semantics for communicating processes with shared variables and its formal encoding in PVS ⋮ Refinement and verification in component-based model-driven design ⋮ Building program construction and verification tools from algebraic principles ⋮ On integrating confidentiality and functionality in a formal method ⋮ Refinement patterns for ASTDs ⋮ The behavioural semantics of Event-B refinement ⋮ Derivation of concurrent programs by stepwise scheduling of Event-B models ⋮ Automated verification of reactive and concurrent programs by calculation ⋮ A UTP semantics for \textsf{Circus} ⋮ Testing for refinement in \textsf{Circus} ⋮ A formal framework for modeling and validating simulink diagrams ⋮ Simulink Timed Models for Program Verification ⋮ Viewing CSP Specifications with UML-RT Diagrams ⋮ Type Checking Specifications ⋮ Laws of mission-based programming

This page was built for software: Circus