OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Event-B at work: some lessons learnt from an application to a robot anti-collision function

Dieumegard, Arnaud and Ge, Ning and Jenn, Eric Event-B at work: some lessons learnt from an application to a robot anti-collision function. (2017) In: NFM (9th NASA Formal Methods Symposium) Formal Methods Symposium, 16 May 2017 - 18 May 2017 (Moffett Field, United States).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://dx.doi.org/10.1007/978-3-319-57288-8_24


The technical and academic aspects of the Event-B method, and the abstract description of its application in industrial contexts are the subjects of numerous publications. In this paper, we describe the experience of development engineers non familiar with Event-B to getting to grips with this method. We describe in details how we used the formalism, the refinement method, and its supporting toolset to develop the simple anti-collision function embedded in a small rolling robot. We show how the model has been developed from a set of high-level requirements and refined down to the software specification. For each phase of the development, we explain how we used the method, expose the encountered difficulties, and draw some practical lessons from this experiment.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer. The definitive version is available at :https://link.springer.com/chapter/10.1007/978-3-319-57288-8_24
HAL Id:hal-01733887
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Other partners > IRT Saint Exupéry - Institut de Recherche Technologique (FRANCE)
Other partners > SYSTEREL (FRANCE)
Deposited On:14 Mar 2018 15:13

Repository Staff Only: item control page