D'Event-B vers UML/OCL en passant par UML/EM-OCL

TL;DR

This paper presents a hybrid development approach combining Event-B and UML/OCL, including an extension to OCL (EM-OCL), demonstrated on an electronic hotel key system case study.

Contribution

It introduces a novel method for transitioning from formal Event-B models to UML/OCL using EM-OCL, enhancing software development for complex systems.

Findings

Feasibility demonstrated on a hotel key system case study

Extension to OCL (EM-OCL) enables transition from formal to semi-formal models

Hybrid approach improves development process for complex software

Abstract

To overcome the limitations of both approaches classical and formal for the development of complex software, we proposed a hybrid approach combining the formal approach (Event-B) and the classical approach (UML/OCL). Upstream phases of our approach include: Rewriting the requirements document, Refinement strategy, Abstract specification and Horizontal refinement. We have shown the feasibility of our approach on a case study: An Electronic Hotel Key System (SCEH). The problem of transition from the formal (Event-B) to the semi-formal (UML/OCL) is processed through our extension to OCL (EM-OCL).