A formal approach for the verification of software composition

by Mohamed GRAIET
DiverSE Coffee
Rennes, France


Hi all, We’re happy to host a DiverSE Coffee this Thursday starring Mohamed GRAIET, an assistant associate professor at ENSAI. Mohamed will be presenting his work on the verification of software composition using the Event-B Method. Enters Mohamed: Reuse is a key concept in building software systems. It enables the composition of a set of existing software to build new ones, with added value. In the context of our work, we are interested in the composition of two types of software, namely Web services and free software based on FOSS (Free and Open Source Software) packages. Despite the research efforts devoted to verification of the correctness Web services and FOSS composition, it remains one of the most difficult tasks. A composite service is said to be correct if it meets a set of requirements of two types: QoS and Transactional requirements. QoS requirements are defined by means of a service-level agreement (SLA), coming in the form of QoS constraints. Whilst, transactional requirements are specified by designers using the concept of Accepted Termination States (ETAs). Finally, A FOSS composite software is said to be correct if it respects a set of constraints on dependencies and capacities. To solve this verification problem, we propose a formal approach based on the Event-B method. This approach can be summed up in two points: (i) Event-B formalization of service composition with Event-B. (ii) Event-B formalization of FOSS software composition in a cloud context. In this talk, I’ll present the proposed approach and elaborate on the different steps involved in the verification process, from formalization to proof. An extended abstract in French can also be found below. This presentation is held in Minquiers at 1 pm.