Event-B Formalization of Event-B Contexts - Assistance à la Certification d’Applications DIstribuées et Embarquées Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

Event-B Formalization of Event-B Contexts

Résumé

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.
Fichier principal
Vignette du fichier
Event-B Formalization Of Event-B Context.pdf (358 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte

Dates et versions

hal-03411227 , version 1 (05-11-2021)

Identifiants

Citer

Jean-Paul Bodeveix, M Filali. Event-B Formalization of Event-B Contexts. 8th International Conference on Rigorous State-Based Methods (ABZ 2021), Jun 2021, Ulm, Germany. pp.66-80, ⟨10.1007/978-3-030-77543-8_5⟩. ⟨hal-03411227⟩
42 Consultations
133 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More