Authors: Imen Tounsi; Mohamed Hadj Kacem; Ahmed Hadj Kacem; Khalil Drira
Addresses: ReDCAD, University of Sfax, Route l'Aéroport Km 0.5, BP 1169 .3029, Sfax, Tunisia ' ReDCAD, University of Sfax, Route l'Aéroport Km 0.5, BP 1169 .3029, Sfax, Tunisia ' ReDCAD, University of Sfax, Route l'Aéroport Km 0.5, BP 1169 .3029, Sfax, Tunisia ' CNRS, LAAS, 7 avenue du colonel Roche, F-31400 Toulouse, France; LAAS, University of Toulouse, F-31400 Toulouse, France
Abstract: Although design patterns have become increasingly popular, most of them are presented in an informal way, which can give rise to ambiguity and may lead to their incorrect usage. Patterns proposed by the SOA design pattern community are described with informal visual notations. Modelling SOA design patterns with a standard formal notation contributes to avoid misunderstanding by software architects and helps endowing design methods with refinement approaches for mastering system architectures complexity. In this paper, we present a formal refinement-based approach that aims, first, to model message-oriented SOA design patterns with the SoaML standard language, and second to formally specify these patterns at a high level of abstraction using the Event-B method. 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 experimented through an example we present in this paper. We implemented our approach under the Rodin platform, which we use to prove model consistency.
Keywords: SOA design patterns; SoaML modelling; formal methods; Event-B method; refinement approach; service-oriented architecture.
International Journal of Cloud Computing, 2015 Vol.4 No.1, pp.78 - 104
Available online: 23 Feb 2015Full-text access for editors Access for subscribers Purchase this article Comment on this article