A Tool-assisted Method for the Systematic Construction of Critical Embedded Systems using Event-B

Pascal André1, Christian Attiogbé1 and Arnaud Lanoix1

  1. LS2N CNRS UMR 6004 - University of Nantes


Embedded control systems combine digital and physical components, leading to complex interactions and even complexity of their development. In [4] we proposed a method to build such complex systems in a systematic way. The overall method starts from an abstract model of the physical environment of the considered system and its controller. The method consists in a sequence of refinement steps, in the spirit of Event-B, that gradually introduces design details from an abstract level, until more concrete levels. Two main refinement processes are distinguished: one to capture the global model, the other to detail it; we provide through the method the guidelines to accompany these two refinement processes. But there were a lack of assistance tools. The designers need to be assisted by tools to guide them, to automate partially the refinements and to help in proving more easily model properties. We illustrate the method with the landing gear system case study and choosing the Event-B tool Rodin for illustration; we make it explicit the tools requirements for such a general method and, we introduce a tool support to assist the user in applying the method in combination with standard Event-B tool such as Rodin

Key words

Embedded control systems; Modelling method; Event-B patterns; Tool

Digital Object Identifier (DOI)


Publication information

Volume 17, Issue 1 (January 2020)
Year of Publication: 2020
ISSN: 1820-0214 (Print) 2406-1018 (Online)
Publisher: ComSIS Consortium

Full text

DownloadAvailable in PDF
Portable Document Format

How to cite

André, P., Attiogbé, C., Lanoix, A.: A Tool-assisted Method for the Systematic Construction of Critical Embedded Systems using Event-B. Computer Science and Information Systems, Vol. 17, No. 1, 315-338. (2020), https://doi.org/10.2298/CSIS123456789X