Formal Modeling for Verifying SCA Dynamic Composition with Event-B

被引：4
|
作者：
Lahouij, Aida [1 ]
Hamel, Lazhar [1 ]
Graiet, Mohamed [1 ]
机构：
[1] High Sch Comp Sci & Math, Monastir, Tunisia
来源：
2015 IEEE 24TH INTERNATIONAL CONFERENCE ON ENABLING TECHNOLOGIES - INFRASTRUCTURE FOR COLLABORATIVE ENTERPRISES | 2015年
关键词：
SCA; Dynamic reconfiguration; Event-B; Formal verification; Dynamic properties; Service selection; Service substitution;
D O I：
10.1109/WETICE.2015.50
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：29 / 34
页数：6
相关论文
共 50 条
  • [11] Formal modelling and verifying of intellectualized information management system using Event-B
    Gao, Hongjiang
    Zhao, Yongsheng
    Liu, Jun
    Qin, Zheng
    [J]. GENERAL SYSTEM AND CONTROL SYSTEM, VOL I, 2007, : 207 - 209
  • [12] Verifying HyperLTL Properties in Event-B
    Bodeveix, Jean-Paul
    Carle, Thomas
    Fares, Elie
    Filali, Mamoun
    Hoang, Thai Son
    [J]. RIGOROUS STATE-BASED METHODS, ABZ 2024, 2024, 14759 : 255 - 261
  • [13] A graphical tool for formal verification using Event-B modeling
    Rahul Karmakar
    [J]. Multimedia Tools and Applications, 2024, 83 : 10899 - 10923
  • [14] A graphical tool for formal verification using Event-B modeling
    Karmakar, Rahul
    [J]. MULTIMEDIA TOOLS AND APPLICATIONS, 2024, 83 (04) : 10899 - 10923
  • [15] Verifying Safety of Behaviour Trees in Event-B
    Tadiello, Matteo
    Troubitsyna, Elena
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2022, (371): : 139 - 155
  • [16] The Composition of Event-B Models
    Poppleton, Michael
    [J]. ABSTRACT STATE MACHINES, B AND Z, PROCEEDINGS, 2008, 5238 : 209 - 222
  • [17] Verifying Composite Service Transactional Behavior with EVENT-B
    Hamel, Lazhar
    Graiet, Mohamed
    Kmimech, Mourad
    Bhiri, Mohamed Tahar
    Gaaloul, Walid
    [J]. SOFTWARE ARCHITECTURE, 2011, 6903 : 67 - 74
  • [18] Modeling and verifying clustering properties in a vehicular ad hoc network protocol with Event-B
    Patrick Sondi
    Imed Abbassi
    Eric Ramat
    Emna Chebbi
    Mohamed Graiet
    [J]. Scientific Reports, 11
  • [19] Verifying Event-B Hybrid Models Using Cyclone
    Wu, Hao
    Cheng, Zheng
    [J]. RIGOROUS STATE-BASED METHODS, ABZ 2023, 2023, 14010 : 179 - 184
  • [20] Modeling and verifying clustering properties in a vehicular ad hoc network protocol with Event-B
    Sondi, Patrick
    Abbassi, Imed
    Ramat, Eric
    Chebbi, Emna
    Graiet, Mohamed
    [J]. SCIENTIFIC REPORTS, 2021, 11 (01)
12345