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 条
  • [31] A CSP account of Event-B refinement
    Schneider, Steve
    Treharne, Helen
    Wehrheim, Heike
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (55): : 139 - 154
  • [32] Event-B patterns and their tool support
    Thai Son Hoang
    Andreas Fürst
    Jean-Raymond Abrial
    Software & Systems Modeling, 2013, 12 : 229 - 244
  • [33] Event-B patterns and their tool support
    Thai Son Hoang
    Fuerst, Andreas
    Abrial, Jean-Raymond
    SOFTWARE AND SYSTEMS MODELING, 2013, 12 (02): : 229 - 244
  • [34] Modelling Hybrid Programs with Event-B
    Afendi, Meryem
    Laleau, Regine
    Mammar, Amel
    RIGOROUS STATE-BASED METHODS, ABZ 2020, 2020, 12071 : 139 - 154
  • [35] Undertaking the Tokeneer Challenge in Event-B
    Rivera, Victor
    Bhattacharya, Sukriti
    Catano, Nestor
    2016 IEEE/ACM 4TH FME WORKSHOP ON FORMAL METHODS IN SOFTWARE ENGINEERING (FORMALISE), 2016, : 8 - 14
  • [36] Event-B Decomposition for Parallel Programs
    Hoang, Thai Son
    Abrial, Jean-Raymond
    ABSTRACT STATE MACHINES, ALLOY, B AND Z, PROCEEDINGS, 2010, 5977 : 319 - 333
  • [37] Automatic Flow Analysis for Event-B
    Bendisposto, Jens
    Leuschel, Michael
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, 2011, 6603 : 50 - 64
  • [38] BUILDING SPECIFICATIONS IN THE EVENT-B INSTITUTION
    Farrell, Marie
    Monahan, Rosemary
    Power, James F.
    LOGICAL METHODS IN COMPUTER SCIENCE, 2021, 18 (04) : 4:1 - 4:55
  • [39] The behavioural semantics of Event-B refinement
    Schneider, Steve
    Treharne, Helen
    Wehrheim, Heike
    FORMAL ASPECTS OF COMPUTING, 2014, 26 (02) : 251 - 280
  • [40] Qualitative probabilistic modelling in Event-B
    Hallerstede, Stefan
    Hoang, Thai Son
    INTEGRATED FORMAL METHODS, PROCEEDINGS, 2007, 4591 : 293 - 312
12345