Using Event-B to Verify the Kmelia Components and Their Assemblies

and formal model, named Kmelia [1,2], with an associated language to specify components, their provided and required services and their assemblies; we also developed a framework named COSTO [3] and re-used some verification tools [1,4] to study the Kmelia specifications. A Kmelia component is equipped with invariants and with pre/post-conditions defined on services. A Kmelia assembly defines a set of links between required and provided services of various components, with respect to their pre/post-conditions. Our main concern is to establish the correctness of Kmelia components and their assemblies. Among the formal analysis necessary to ensure complete correctness, we consider: (i) the component invariant consistency vs. pre-/post-conditions of services; (ii) the Kmelia assembly link contract correctness, that relates services which are linked in the assemblies. We use the notion of contract as in the classical works and results such as design-by-contract [5] or specification mat...

• Type: Conference
• Year: 2010
• Where: ASM
• Authors: Pascal André, Gilles Ardourel, Christian Attiogbé, Arnaud Lanoix
• Keywords: ASM 2010, Kmelia Components, Microbiology, Proof Obligations, Required Service