Specification and Verification of Communication Paradigms for CBSE in Event B

The development of distributed computing systems and of their usage in domains such as the Internet of Things, Big Data, etc., raises numerous questions on the tools available to model the complexity of such systems. Non-formal modeling methods fail to create a rigorous way to describe and analyze these systems. In this paper, we propose an approach to model and analyze the structural and behavioural aspect of these systems using formal techniques. As a prerequisite, we build reusable model libraries to specify and verify communication paradigms for modeling software architectures of distributed systems in a component-based system engineering (CBSE) context. First, we describe high-level concepts for system architecture in a component-port-connector fashion as a metamodel. Then, we develop an Event-B interpretation of the metamodel adding communication characteristics such as buffering, FIFO and synchronicity. To validate our work, we studied the two well-known communication paradigms, namely message passing and remote procedure call.