Relaxing b sharing restrictions within CSP||B

This paper addresses the issue of state sharing in CSP||B specifications: B machines controlled by various CSP parts are supposed not to refer to, share or modify the same state space. However, some kinds of B state sharing can be allowed without creating inconsistencies in CSP||B specifications. To achieve this, we present a B-based solution for allowing architectures with B state sharing in the CSP||B components. We show that the inconsistencies in state sharing can be identified by translating the CSP controllers into B specifications and then using a more refined consistency checking process. We also hint at possible extensions towards other CSP||B architectural patterns with various types of sub-components sharing.