An Event-B Development Process for the Distributed BIP Framework

Abstract : We present a refinement-based methodology to design correct by construction distributed systems specified as Event-B models. Starting from an Event-B machine, the studied process proposes successive steps in order to split and schedule the computation of complex events and then to map them on subcomponents. The specification of these steps is done through two domain specific languages. From these specifications, two refinements are generated. Eventually, a distributed code architecture is also generated. The correctness of the process relies on the correctness of the refinements and the translation. We target the distributed BIP framework.
Keywords : Embedded systems
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01709119
Contributor : Open Archive Toulouse Archive Ouverte (oatao) <>
Submitted on : Wednesday, February 14, 2018 - 3:50:22 PM
Last modification on : Thursday, October 24, 2019 - 2:44:06 PM
Long-term archiving on: Monday, May 7, 2018 - 6:35:09 PM

File

siala_18825.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01709119, version 1
  • OATAO : 18825

Citation

Badr Siala, Tahar Bhiri, Jean-Paul Bodeveix, Mamoun Filali. An Event-B Development Process for the Distributed BIP Framework. 18th International Conference on Formal Engineering Methods (ICFEM 2016), Nov 2016, Tokyo, Japan. pp. 313-328. ⟨hal-01709119⟩

Share

Metrics

Record views

70

Files downloads

131