On the Benefits of Using MVC Pattern for Structuring Event-B Models of WIMP Interactive Applications. Issue 1 (10th May 2021)

• Record Type: Journal Article
• Authors: Singh, Neeraj Kumar; Aït-Ameur, Yamine; Geniet, Romain; Méry, Dominique; Palanque, Philippe
• Is Part Of: Interacting with computers. Volume 33:Issue 1(2021)
• Page Start: 92
• Page End: 114
• Publication Date: 2021-05-10
• Subjects: formal description techniques -- interactive applications -- model-view-controller -- refinement and proofs -- Event-B -- safety-critical interactive systems; Human-computer interaction -- Periodicals; 004.019
• DOI: 10.1093/iwcomp/iwab016
• Languages: English
• ISSNs: 0953-5438

Abstract

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.