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
关键词
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 条
  • [21] Formal Verification of AADL Models by Event-B
    Hadad, Abeer Saeed Abdo
    Ma, Chunyan
    Ahmed, Adeeb Abdulwakeel Obadi
    [J]. IEEE ACCESS, 2020, 8 : 72814 - 72834
  • [22] Research on Event-B based formal modeling and verification of automatic production line
    Fu, Kaiming
    Fang, Bin
    Li, Yafen
    Li, Huijie
    [J]. PROCEEDINGS OF THE 28TH CHINESE CONTROL AND DECISION CONFERENCE (2016 CCDC), 2016, : 3690 - 3695
  • [23] Formal modeling and analysis of ad hoc Zone Routing Protocol in Event-B
    Chunyan Fu
    Kougen Zheng
    [J]. International Journal on Software Tools for Technology Transfer, 2019, 21 : 165 - 181
  • [24] Formal Modelling of Domain Constraints in Event-B
    Mohand-Oussaid, Linda
    Ait-Sadoune, Idir
    [J]. MODEL AND DATA ENGINEERING (MEDI 2017), 2017, 10563 : 153 - 166
  • [25] Formal Verification of a Medical Insurance System Prototype: The Event-B Modeling Approach
    Karmakar, Rahul
    Dutta, Saheli
    [J]. JOURNAL OF INFORMATION ASSURANCE AND SECURITY, 2022, 17 (01): : 25 - 34
  • [26] Formal modeling and analysis of ad hoc Zone Routing Protocol in Event-B
    Fu, Chunyan
    Zheng, Kougen
    [J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2019, 21 (02) : 165 - 181
  • [27] Towards the Composition of Specifications in Event-B
    Silva, Renato
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2011, 280 : 81 - 93
  • [28] Modeling of TCP Protocol in Event-B
    Wang, Xue-Jing
    Zhang, Hong
    [J]. INFORMATION TECHNOLOGY APPLICATIONS IN INDUSTRY, PTS 1-4, 2013, 263-266 : 1156 - 1159
  • [29] Formal analysis of imprecise system requirements with Event-B
    Hong Anh Le
    Nakajima, Shin
    Ninh Thuan Truong
    [J]. SPRINGERPLUS, 2016, 5
  • [30] Formal Analysis of BPMN Models Using Event-B
    Bryans, Jeremy W.
    Wei, Wei
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, 2010, 6371 : 33 - +