Using SoaML Models and Event-B Specifications for Modeling SOA Design Patterns

Imen Tounsi (1) , Hrichi Zied (1) , Mohamed Hadj Kacem (2) , Ahmed Hadj Kacem (1) , Khalil Drira (3)

1 REDCAD - Unité de Recherche en développement et contrôle d'applications distribuées
2 ReDCAD
3 LAAS-SARA - Équipe Services et Architectures pour Réseaux Avancés

Although design patterns have become increasingly popular, most of them are presented in an informal way. Patterns, proposed by the SOA design pattern community, are described with a proprietary informal notation, which can raise ambiguity and may lead to their incorrect usage. Modeling SOA design patterns with a standard formal notation avoids misunderstanding by software architects and helps endow design methods. In this paper, we present an approach that aims, first, to model message-oriented SOA design patterns with the SoaML language, and second to transform them to Event-B specifications. These two steps are performed before undertaking the effective coding of a design pattern providing correct by construction pattern-based software architectures. Our approach is enhanced with a tool supporting it. Specification results are imported under the Rodin platform which we use to prove model consistency.

Mots clés: SOA Design patterns: SoaML modeling: Formal methods: Event-B method: Tool support

Domaines: Architectures Matérielles [cs.AR]

Imen Tounsi, Hrichi Zied, Mohamed Hadj Kacem, Ahmed Hadj Kacem, Khalil Drira. Using SoaML Models and Event-B Specifications for Modeling SOA Design Patterns. International Conference on Enterprise Information Systems (ICEIS), Jul 2013, Angers, France. 11p. ⟨hal-00801025⟩