Extensible Record Structures in Event-B

被引：1
|
作者：
Fathabadi, Asieh Salehi [1 ]
Snook, Colin [1 ]
Hoang, Thai Son [1 ]
Dghaym, Dana [1 ]
Butler, Michael [1 ]
机构：
[1] Univ Southampton, ECS, Southampton, Hants, England
来源：
RIGOROUS STATE-BASED METHODS, ABZ 2021 | 2021年 / 12709卷
关键词：
D O I：
10.1007/978-3-030-77543-8_12
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Event-B is a state-based formal method for system development. The Event-B mathematical language does not support a syntax for the direct definition of structured types such as records. This paper proposes extending the Event-B language with direct record definitions. A key feature is the ability to extend records with new fields in refinement steps. The XEvent-B tool, which supports a textual representation of Event-B models, is extended to provide support for direct record definition and automatic transformation of record structures into standard Event-B elements. We demonstrate this work by modelling of the Tokeneer case study.
引用
收藏
页码：130 / 136
页数：7
相关论文
共 50 条
  • [1] An open extensible tool environment for event-B
    Abrial, Jean-Raymond
    Butler, Michael
    Hallerstede, Stefan
    Voisin, Laurent
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2006, 4260 : 588 - 605
  • [2] Decomposition Structures for Event-B
    Butler, Michael
    INTEGRATED FORMAL METHODS, PROCEEDINGS, 2009, 5423 : 20 - 38
  • [3] Event-B Formalization of Event-B Contexts
    Bodeveix, Jean-Paul
    Filali, Mamoun
    RIGOROUS STATE-BASED METHODS, ABZ 2021, 2021, 12709 : 66 - 80
  • [4] A Graphical Tool for Event Refinement Structures in Event-B
    Dghaym, Dana
    Trindade, Matheus Garay
    Butler, Michael
    Fathabadi, Asieh Salehi
    ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016), 2016, 9675 : 269 - 274
  • [5] Language and tool support for event refinement structures in Event-B
    Fathabadi, Asieh Salehi
    Butler, Michael
    Rezazadeh, Abdolbaghi
    FORMAL ASPECTS OF COMPUTING, 2015, 27 (03) : 499 - 523
  • [6] Derivation of algorithmic control structures in Event-B refinement
    Dalvandi, Mohammadsadegh
    Butler, Michael
    Rezazadeh, Abdolbaghi
    SCIENCE OF COMPUTER PROGRAMMING, 2017, 148 : 49 - 65
  • [7] Core Hybrid Event-B I: Single Hybrid Event-B machines
    Banach, Richard
    Butler, Michael
    Qin, Shengchao
    Verma, Nitika
    Zhu, Huibiao
    SCIENCE OF COMPUTER PROGRAMMING, 2015, 105 : 92 - 123
  • [8] Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water Tanks
    Banach, Richard
    Butler, Michael
    FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2016, 2016, 10009 : 90 - 105
  • [9] Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines
    Banach, Richard
    Butler, Michael
    Qin, Shengchao
    Zhu, Huibiao
    SCIENCE OF COMPUTER PROGRAMMING, 2017, 139 : 1 - 35
  • [10] Enabling Analysis for Event-B
    Dobrikov, Ivaylo
    Leuschel, Michael
    ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016), 2016, 9675 : 102 - 118
12345