The semantics of Circus

DOI10.1007/3-540-45648-1_10MaRDI QIDQ4472182zbMATH OpenFDO

Authors Ana Cavalcanti, Jim Woodcock

Publication date 3 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2272/22720184.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• A refinement strategy for Circus
• A UTP semantics for \textsf{Circus}
• FM 2005: Formal Methods
• scientific article; zbMATH DE number 2090152
• Refinement of actions in Circus

Cited in

(37)

• A UTP semantics for \textsf{Circus}
• A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
• Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
• Efficient symbolic computation of process expressions
• A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
• A CSP model of Eiffel's SCOOP
• Responsiveness and stable revivals
• Three Approaches to Timed External Choice in UTP
• Isabelle/UTP: a mechanised theory engineering framework
• Towards Algebraic Semantics of Circus Time
• Simulink timed models for program verification
• Semantic domains for Handel-C
• Refinement of actions in Circus
• Type checking \textsf{Circus} specifications
• Building a Modal Interface Theory for Concurrency and Data
• rCOS: defining meanings of component-based software architectures
• Unifying theories of programming in Isabelle
• A two-way path between formal and informal design of embedded systems
• CSP with Hierarchical State
• scientific article; zbMATH DE number 2090152 (Why is no real title available?)
• A denotational semantics for Handel-C
• Interface theories for concurrency and data
• A semantics for behavior trees using CSP with specification commands
• FM 2005: Formal Methods
• UTP, \textsf{\textit{Circus}}, and Isabelle
• \textit{\textsf{Circus2CSP}}: a tool for model-checking \textit{\textsf{Circus}} using FDR
• An operational semantics in Isabelle/HOL-CSP
• Formal verification of BDI agents
• A refinement strategy for Circus
• Isabelle/Circus
• On integrating confidentiality and functionality in a formal method
• Refinement patterns for ASTDs
• The behavioural semantics of Event-B refinement
• Cameo: an alternative model of concurrency for Eiffel
• Angelic nondeterminism in the unifying theories of programming
• Denotational semantics and its algebraic derivation for an event-driven system-level language
• A timeband framework for modelling real-time systems

Describes a project that uses

Uses Software

• Circus

This page was built for publication: The semantics of Circus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4472182)