From an abstract specification in event-b toward an UML/OCL model
Imen Sayar, Mohamed Tahar Bhiri · 2014
The formal approach of software development promotes getting proved correct software. It faces the shortcomings of the classical approach concerning the ambiguity of the requirements document, the risk of errors distributed to all phases and the high testing cost (because of late detection of such errors). However, this approach poses problems mainly related to the participation of various actors not necessarily professionals in formal methods, maintenance and especially the development of an "optimal" refinement strategy. To overcome the limitations of these two approaches, we propose a hybrid approach that combines 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, Horizontal refinement and Validation. Downstream phases contain the Construction of a UML/EM-OCL model, Refinement, Integration of design and implementation decisions, Coding and Integration. In this paper, we show the feasibility of our approach on a case study: An Electronic Hotel Key System (SCEH). The problem of transition from formal (Event-B) to the semi-formal (UML/OCL) is processed by our OCL extension called EM-OCL.