Composing Specications using Communication

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 communi cating 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 compo sitionally verify it and show that it is a re speci cation described in CSP This allows safety and liveness properties to be established for combinations of communicating B machine