HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

On the Benefits of Using MVC Pattern for Structuring Event-B Models of WIMP Interactive Applications

Abstract : This paper presents a formal development approach for designing interactive applications using a correct-by-construction approach. In this work, we propose a refinement strategy using model-view-controller (MVC) to structure and design Event-B formal models of the interactive application. The proposed MVC-based refinement strategy facilitates the development of an abstract model and a series of refined models by introducing the possible modes, controller’s behaviour and visual components of the interactive application while preserving the required interaction-related safety properties. To demonstrate the effectiveness, scalability, reliability and feasibility of our approach, we use a small example (from automotive domain) and real-life industrial case studies (from aviation). The entire development is realized in Event-B and the associated Rodin tool is used to analyse and verify the correctness of the formalized model. Finally, the developed Event-B models are used to generate source code using EB2ALL tool for going from the specification to the implementation of the interactive application.
Complete list of metadata

Contributor : Dominique Méry Connect in order to contact the contributor
Submitted on : Tuesday, May 11, 2021 - 11:27:26 PM
Last modification on : Friday, April 1, 2022 - 3:44:45 AM



Neeraj Kumar Singh, Yamine Aït-Ameur, Romain Geniet, Dominique Méry, Philippe Palanque. On the Benefits of Using MVC Pattern for Structuring Event-B Models of WIMP Interactive Applications. Interacting with Computers, Oxford University Press (OUP), 2021, ⟨10.1093/iwcomp/iwab016⟩. ⟨hal-03224780⟩



Record views