Preuve de cohérence de composants Kmelia à l'aide de la méthode B

National audiencePour répondre aux objectifs de qualité dans la construction de systèmes à base de composants logiciels et améliorer la confiance dans les composants et leur assemblage, il est nécessaire de disposer d'un Kmelia est un modèle à composants multi-services dans lequel les composants sont abstraits et formels de façon à pouvoir y exprimer des propriétés et les vérifier. Dans cet article nous étudions l'automatisation de la vérification de cohérence des composants Kmelia et de leur assemblage en nous servant de la méthode \B. Pour ce faire, des machines \B sont extraites des composants Kmelia et vérifiées en utilisant l'Atelier B, établissant de fait les propriétés au niveau de Kmelia. La démarche est illustrée par un exemple de gestion de stock