Modélisation et vérification formelles en B d’architectures logicielles à trois niveaux

Abderrahman Mokni (1) , Marianne Huchard (2) , Christelle Urtado (1) , Sylvain Vauttier (1) , Huaxi Yulin Zhang (3)

1 LGI2P - Laboratoire de Génie Informatique et Ingénierie de Production
2 MAREL - Models And Reuse Engineering, Languages
3 Inria - Institut National de Recherche en Informatique et en Automatique

La réutilisation est une notion centrale dans le développement à base de composants. Elle permet de construire des logiciels à grande échelle de meilleure qualité et à moindre coût. Afin d’intensifier la réutilisation dans les processus de développement, un ADL à trois dimensions, nommé Dedal, a été proposé. Dedal permet de décrire la spécification, l’implémentation et le déploiement d’une architecture. Chaque définition doit être cohérente, complète et, réutilisant la définition de niveau supérieur, conforme à celle-ci. Cet article présente des règles formelles permettant de préserver et de vérifier ces trois propriétés dans des définitions d’architectures décrites en Dedal. Les règles sont exprimées avec le langage formel B afin d’automatiser leur vérification.

Domaines: Génie logiciel [cs.SE]

Abderrahman Mokni, Marianne Huchard, Christelle Urtado, Sylvain Vauttier, Huaxi Yulin Zhang. Modélisation et vérification formelles en B d’architectures logicielles à trois niveaux. CIEL: Conférence en IngénieriE du Logiciel, Jun 2014, Paris, France. pp.71-77. ⟨hal-01244431⟩