Automatic Refinement for Event-B through Annotated Patterns

Badr Siala; Jean-Paul Bodeveix; Mamoun Filali; Tahar Bhiri

Automatic Refinement for Event-B through Annotated Patterns

Badr Siala ^{1, 2} Jean-Paul Bodeveix ¹ Mamoun Filali ¹ Tahar Bhiri ²

1 IRIT - Institut de recherche en informatique de Toulouse

2 Université de Sfax - University of Sfax

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 : Formal methods Distributed systems Correct by construction Event-B BIP Patterns

Document type :

Conference papers

Domain :

Computer Science [cs] / Software Engineering [cs.SE]

Computer Science [cs] / Embedded Systems

Computer Science [cs] / Cryptography and Security [cs.CR]

Computer Science [cs] / Human-Computer Interaction [cs.HC]

Computer Science [cs] / Hardware Architecture [cs.AR]

Computer Science [cs] / Modeling and Simulation

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 : Friday, January 10, 2020 - 9:09:25 PM
Long-term archiving on: Saturday, January 5, 2019 - 4:06:04 PM

siala_19076.pdf

Files produced by the author(s)

Automatic Refinement for Event-B through Annotated Patterns

File

Identifiers

Collections

Citation

Export

Metrics

48

120

CONTACT

Automatic Refinement for Event-B through Annotated Patterns

File

Identifiers

Collections

Citation

Export

Share

Metrics

48

120

CONTACT