Formal Modeling for Verifying SCA Dynamic Composition with Event-B

Author

Lahouij, Aida ; Hamel, Lazhar ; Graiet, Mohamed

Author_Institution

High Sch. of Comput. Sci. & Math., Monastir, Tunisia

fYear

2015

Firstpage

29

Lastpage

34

Abstract

Service Component Architecture (SCA) is a set of specifications which describe a model for building applications and systems using a Service-Oriented Architecture (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 context, we intend to propose an Event-B based approach so as to configure the SCA composition dynamically. We focus, particularly, on the correctional dynamic such as substituting faulty services and components. The consistency and the validity of the obtained model have been proved by the Event-B dedicated tools.

Keywords

formal specification; formal verification; service-oriented architecture; Event-B based approach; SCA composition specification; SCA dynamic composition verification; SCA specification; SOA; formal modeling; service component architecture; service-oriented architecture; Assembly; Business; Context; Protocols; Quality of service; Service-oriented architecture; Wires; Dynamic properties; Dynamic reconfiguration; Event-B; Formal verification; SCA; Service selection; Service substitution;

fLanguage

English

Publisher

ieee

Conference_Titel

Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), 2015 IEEE 24th International Conference on

Conference_Location

Larnaca

Type

conf

DOI

10.1109/WETICE.2015.50

Filename

7194324