Title :
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
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;
Conference_Titel :
Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), 2015 IEEE 24th International Conference on
Conference_Location :
Larnaca
DOI :
10.1109/WETICE.2015.50
