CSP theorems for communicating B machines

DOI10.1007/S00165-005-0076-7MaRDI QIDQ2432218zbMATH OpenOpenAlexDBLPWikidataFDO

Authors S. A. Schneider, Helen Treharne

Publication date 25 October 2006

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL http://epubs.surrey.ac.uk/7238/2/fullifm.pdf

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Computer system organization (68M99)

Recommendations

• Integrated Formal Methods
• scientific article; zbMATH DE number 2080013
• csp2B: A practical approach to combining CSP and B
• scientific article; zbMATH DE number 2013575
• Interactive tool support for CSP \(\parallel\) B consistency checking

Cited in

(19)

• A semantics for behavior trees using CSP with specification commands
• Responsiveness and stable revivals
• Changing system interfaces consistently: a new refinement strategy for CSP\(\|\)B
• Verification of \(\mathrm{EB}^3\) specifications using CADP
• Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B
• Laws of mission-based programming
• csp2B: A practical approach to combining CSP and B
• Relational concurrent refinement. II: Internal operations and outputs
• Reasoning about resources in the embedded systems language Hume
• Integrated Formal Methods
• UTP, \textsf{\textit{Circus}}, and Isabelle
• scientific article; zbMATH DE number 2080013 (Why is no real title available?)
• FM 2005: Formal Methods
• The behavioural semantics of Event-B refinement
• Chunks: Component Verification in CSP ∥ B
• A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
• Hume box calculus: Robust system development through software transformation
• Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans
• Interactive tool support for CSP \(\parallel\) B consistency checking

Describes a project that uses

Uses Software

• ProB
• csp2B

This page was built for publication: CSP theorems for communicating B machines

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