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 条
  • [41] A CSP Approach to Control in Event-B
    Schneider, Steve
    Treharne, Helen
    Wehrheim, Heike
    INTEGRATED FORMAL METHODS, 2010, 6396 : 260 - +
  • [42] Concurrent Scheduling of Event-B Models
    Bostrom, Pontus
    Degerlund, Fredrik
    Sere, Kaisa
    Walden, Marina
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (55): : 166 - 182
  • [43] Event-B method and liveness properties
    Mosbahi O.
    Jaray J.
    Journal Europeen des Systemes Automatises, 2010, 44 (9-10): : 1119 - 1163
  • [44] A LTS Approach to Control in Event-B
    Peng, Han
    Du, Chenglie
    Rao, Lei
    Chen, Fu
    SCIENTIFIC PROGRAMMING, 2018, 2018
  • [45] Towards the Composition of Specifications in Event-B
    Silva, Renato
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2011, 280 : 81 - 93
  • [46] External and internal choice with event groups in Event-B
    Butler, Michael
    FORMAL ASPECTS OF COMPUTING, 2012, 24 (4-6) : 555 - 567
  • [47] Incremental System Modelling in Event-B
    Hallerstede, Stefan
    FORMAL METHODS FOR COMPONENTS AND OBJECTS, 2009, 5751 : 139 - 158
  • [48] Analysis of DSR Protocol in Event-B
    Mery, Dominique
    Singh, Neeraj Kumar
    STABILIZATION, SAFETY, AND SECURITY OF DISTRIBUTED SYSTEMS, 2011, 6976 : 401 - 415
  • [49] On the purpose of Event-B proof obligations
    Hallerstede, Stefan
    FORMAL ASPECTS OF COMPUTING, 2011, 23 (01) : 133 - 150
  • [50] Templates for Event-B Code Generation
    Edmunds, Andrew
    ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z, ABZ 2014, 2014, 8477 : 284 - 289
12345