Multi-levels Use of Contracts for Trusted Components

International audienceWe present in the article a formal approach for handling and analysing contracts in component model early in development process. Contracts are helpful to describe component interoperability levels. This work is founded on the correctness-by-construction methodology with the aim to assist in building correct complex systems. The approach is illustrated on the Kmelia component model and on the COSTO framework, an Eclipse plugin, which supports user friendly editing, and verication of Kmelia contracts by roviding various bridges with efficient external tools. A case study is presented as illustration of our approach