On the Benefits of Using MVC Pattern for Structuring Event-B Models of WIMP Interactive Applications - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Interacting with Computers Année : 2021

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

Résumé

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.
Fichier non déposé

Dates et versions

hal-03224780 , version 1 (11-05-2021)

Identifiants

Citer

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, 2021, ⟨10.1093/iwcomp/iwab016⟩. ⟨hal-03224780⟩
113 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More