Published in

Springer Verlag, Lecture Notes in Computer Science, p. 58-78

DOI: 10.1007/3-540-44880-2_5

Links

Tools

Export citation

Search in Google Scholar

Composing Specifications Using Communication

Journal article published in 2003 by Helen Treharne, Steve A. Schneider, Marchia Bramble
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Green circle
Preprint: archiving allowed
Green circle
Postprint: archiving allowed
Red circle
Published version: archiving forbidden
Data provided by SHERPA/RoMEO

Abstract

This paper develops a case study using the process algebra CSP to enable controlled interaction between B machines. This illustrates how B machines are essential components within a combined communicating system. The development steps used to build the case study are new: they are applications of theoretical results which allow us to focus on the external interface of a combined communicating system, compositionally verify it, and show that it is a refinement of a more abstract specification described in CSP. This allows safety and liveness properties to be established for combinations of communicating B machines