Mobile CSP||B

Abstract

CSP||B is a combination of CSP and B in which CSP processes are used as control executives for B machines. This architecture enables a B machine and its controller to interact and communicate with each other while working in parallel. The architecture has focused on sequential CSP processes as dedicated controllers for B machines. This paper introduces Mobile CSP||B, a formal framework based on CSP||B which enables us to specify and verify concurrent systems with mobile architecture instead of the previous static architecture. In Mobile CSP||B, a parallel combination of CSP processes act as the control executive for the B machines and these B machines can be transferred between CSP processes during the system execution. The paper introduces the foundations of the approach, and illustrates the result with an example.