Skip to Main content Skip to Navigation
Conference papers

Automatic Refinement for Event-B through Annotated Patterns

Badr Siala 1, 2 Jean-Paul Bodeveix 3 Mamoun Filali 3 Tahar Bhiri 2
1 IRIT - Institut de recherche en informatique de Toulouse
2 Université de Sfax - University of Sfax
3 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
IRIT - Institut de recherche en informatique de Toulouse
Abstract : In this paper, we investigate how patterns could be used in order to generate Event-B refinements automatically through DSL(s) for temporal, timed or distribution patterns. Our ultimate goal is to generate code for a concurrent, or distributed framework, e.g., BIP.
Keywords : Correct by construction Event-B BIP Patterns Formal methods Distributed systems
Document type :
Conference papers
Complete list of metadatas

Cited literature [8 references]  Display  Hide  Download
https://hal.archives-ouvertes.fr/hal-01887899
Contributor : Open Archive Toulouse Archive Ouverte (oatao) <>
Submitted on : Thursday, October 4, 2018 - 3:32:38 PM
Last modification on : Tuesday, January 5, 2021 - 2:22:03 PM
Long-term archiving on: : Saturday, January 5, 2019 - 4:06:04 PM

File

Vignette du document
siala_19076.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01887899, version 1
  • OATAO : 19076

Collections

CNRS | TDS-MACS | SMS | UNIV-TLSE2 | UNIV-TLSE3 | UT1-CAPITOLE | IRIT | IRIT-ACADIE

Citation

Badr Siala, Jean-Paul Bodeveix, Mamoun Filali, Tahar Bhiri. Automatic Refinement for Event-B through Annotated Patterns. 25th Euromicro International Conference on Parallel, Distributed and network-based Processing (PDP 2017), Mar 2017, Saint Petersburg, Russia. pp. 287-290. ⟨hal-01887899⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

117

Files downloads

292

CONTACT

scd.ao@univ-tlse3.fr