Event-B Formalization of Event-B Contexts

被引：5
|
作者：
Bodeveix, Jean-Paul [1 ]
Filali, Mamoun [2 ]
机构：
[1] IRIT UPS, 118 Route Narbonne, F-31062 Toulouse, France
[2] IRIT CNRS, 118 Route Narbonne, F-31062 Toulouse, France
来源：
RIGOROUS STATE-BASED METHODS, ABZ 2021 | 2021年 / 12709卷
关键词：
Formal methods; Event-B; Meta modelisation;
D O I：
10.1007/978-3-030-77543-8_5
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This paper presents an Event-B meta-modelisation of an Event-B project restricted to its context hierarchy which introduces the functional part of a development through sets, constants, axioms and theorems. We study the proposal of a new mechanism for Event-B. It consists in allowing to instantiate in a new context an already proved theorem in a given context. We investigate the validation of the instantiation mechanism in order to prove the validity of imported theorems. We also compare the proposal with similar mechanisms available within some existing theorem provers.
引用
收藏
页码：66 / 80
页数：15
相关论文
共 50 条
  • [1] Event-B Formalization of Basic Supply Chain Patterns
    Saksupawattanakul, Chalika
    Vatanawood, Wiwat
    2018 19TH IEEE/ACIS INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, ARTIFICIAL INTELLIGENCE, NETWORKING AND PARALLEL/DISTRIBUTED COMPUTING (SNPD), 2018, : 352 - 357
  • [2] AR2B: FORMALIZATION OF ARABIC TEXTS WITH EVENT-B
    Ossoukine, Kheira-Zineb Bousmaha
    Hadrich, Lamia Belguith
    JORDANIAN JOURNAL OF COMPUTERS AND INFORMATION TECHNOLOGY, 2020, 6 (02): : 148 - 164
  • [3] 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
  • [4] 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
  • [5] Semantics Formalisation - From Event-B Contexts to Theories
    Thai Son Hoang
    Voisin, Laurent
    Wright, Karla Vanessa Morris
    Snook, Colin
    Butler, Michael
    RIGOROUS STATE-BASED METHODS, ABZ 2024, 2024, 14759 : 208 - 214
  • [6] A formal model for output multimodal HCI An Event-B formalization
    Mohand-Oussaid, Linda
    Ait-Sadoune, Idir
    Ait-Ameur, Yamine
    Ahmed-Nacer, Mohamed
    COMPUTING, 2015, 97 (07) : 713 - 740
  • [7] A formal model for output multimodal HCIAn Event-B formalization
    Linda Mohand-Oussaid
    Idir Ait-Sadoune
    Yamine Ait-Ameur
    Mohamed Ahmed-Nacer
    Computing, 2015, 97 : 713 - 740
  • [8] 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
  • [9] Enabling Analysis for Event-B
    Dobrikov, Ivaylo
    Leuschel, Michael
    ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016), 2016, 9675 : 102 - 118
  • [10] A proposal for records in Event-B
    Evans, Neil
    Butler, Michael
    FM 2006: FORMAL METHODS, PROCEEDINGS, 2006, 4085 : 221 - 235
12345