Sciweavers

ASM
2010
ASM

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

14 years 5 months ago
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...
Pascal André, Gilles Ardourel, Christian At
Added 28 May 2010
Updated 28 May 2010
Type Conference
Year 2010
Where ASM
Authors Pascal André, Gilles Ardourel, Christian Attiogbé, Arnaud Lanoix
Comments (0)