Reactivising Classical B

Abstract

We propose what is essentially a recasting of Circus, the Z-and-CSP-based concurrent language for refinement, into a B context by means of a modest extension of classical B which introduces a new structural component called a reactive-B process. This specifies the channels via which the process can communicate with its environment, and actions by which its behaviour is specified. Such actions are expressed in a new action notation in the same syntactic spirit as B’s Abstract Machine Notation, but with a similar Unifying Theories of Programming relational semantics to that of the actions of Circus. Crucially, by including ordinary abstract machines these reactive-B processes can also acquire persistent state, which their actions can manipulate by invoking the operations of those included machines.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{DunneZ10,
  author       = {Steve Dunne and
                  Frank Zeyda},
  editor       = {Marc Frappier and
                  Uwe Gl{\"{a}}sser and
                  Sarfraz Khurshid and
                  R{\'{e}}gine Laleau and
                  Steve Reeves},
  title        = {Reactivising Classical {B}},
  booktitle    = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
                  {ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5977},
  pages        = {302--318},
  publisher    = {Springer},
  year         = {2010},
  url          = {https://doi.org/10.1007/978-3-642-11811-1\_23},
  doi          = {10.1007/978-3-642-11811-1\_23},
  timestamp    = {Mon, 05 Feb 2024 20:35:41 +0100},
  biburl       = {https://dblp.org/rec/conf/asm/DunneZ10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}