Affordable Access

deepdyve-link
Publisher Website

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

Authors
  • Singh, Neeraj Kumar
  • Aït-Ameur, Yamine
  • Geniet, Romain
  • Méry, Dominique
  • Palanque, Philippe
Publication Date
May 10, 2021
Identifiers
DOI: 10.1093/iwcomp/iwab016
OAI: oai:HAL:hal-03224780v1
Source
HAL
Keywords
Language
English
License
Unknown
External links

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.

Report this publication

Statistics

Seen <100 times