A Tool-assisted Method for the Systematic Construction of Critical Embedded Systems using Event-B
- LS2N CNRS UMR 6004 - University of Nantes
{firstname.lastname}@univ-nantes.fr
Abstract
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)
https://doi.org/10.2298/CSIS123456789X
Publication information
Volume 17, Issue 1 (January 2020)
Year of Publication: 2020
ISSN: 2406-1018 (Online)
Publisher: ComSIS Consortium
Full text
Available 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