Formal Verification of SCA Assembly Model with Event-B

Author

Lahouij, Aida ; Hamel, Lazhar ; Graiet, Mohamed

Author_Institution

FSM, Monastir Univ., Monastir, Tunisia

fYear

2013

fDate

3-4 Oct. 2013

Firstpage

44

Lastpage

51

Abstract

Service Component Architecture (SCA) is a new promising programming model for constructing service-oriented application, which facilitates the development of business integration in SOA. However, SCA in its current form does not represent any formal definition. In addition, there is a growing interest for verification techniques which help to prevent SCA composition specification failure. In this paper, firstly, we present an Event-B model for formal representation and verification of an SCA based composition. And then, we extend this model in order to automate the transformation and the verification of the SCA assembly by the implantation of an Eclipse plug-in.

Keywords

formal specification; formal verification; service-oriented architecture; Eclipse plug-in; Event-B; SCA assembly model; SCA composition specification failure; SOA; business integration; formal definition; formal representation; formal verification; programming model; service component architecture; service-oriented application; service-oriented architecture; Assembly; Business; Context; Context modeling; Mathematical model; Unified modeling language; Wires; Assembly model; Event-B; SCA; Verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Semantics, Knowledge and Grids (SKG), 2013 Ninth International Conference on

Conference_Location

Beijing

Type

conf

DOI

10.1109/SKG.2013.31

Filename

6816583