Formal modeling for verifying SCA composition

With the emergence of Service Component Architecture (SCA), all interests were focused on representing this architecture in a formal way in order to be able to prevent the specifications failures. In this context, our recent works were interested in formalising structural properties of the SCA specifications, particularly to defining structural compatibility between connected services. In fact, verifying structural compatibility is necessary but not sufficient. In this paper we intend to represent, in a first step, the SCA behavioral properties by means of Event-B invariants and events. In a second step, we established behavioral compatibility between services interacting together which is considered as a delicate task and has a great importance in guaranteeing reliable communication between services. At last, we propose an Event-B based approach so as to configure the SCA composition dynamically. We focus, particularly, on the correctional dynamic such as substituting faulty services and components. The consistency and the validity of the obtained model have been proved by the Event-B dedicated tools.