Graphical Transformations of OWL Ontology to Event-B Formal Models

Tracking #: 2209-3422

This paper is currently under review
Eman Alkhammash

Responsible editor: 
Rafael Goncalves

Submission type: 
Full Paper
Formal methods use mathematical models for developing systems. The creation of formal models from informal requirements demands skills and effort since this involves major problems such as ambiguity, inconsistency, and imprecision. To tackle this, it is necessary to have methods and approaches to support mapping requirements of formal specifications. This paper aims to present an approach that addresses this challenge by using the W3C Web Ontology Language (OWL) to construct Event-B formal models. OWL ontologies provide the formal notion that capture domain models. Recently, research on requirements engineering have shown an increased interest in using ontologies in various phases of requirements engineering. Our approach reduces the burden of dealing with formal notations of OWL ontologies and Event-B models and aims to harness the power of OWL ontologies to construct Event-B models using diagrams. The idea is based on the transformation of OntoGraf diagrams of OWL ontologies to UML-B diagrams to bridge the gap between OWL ontologies and Event-B models. OntoGraf is used to visualise ontology knowledge, whereas UML-B provides diagrammatic modelling notations for creating Event-B models. Event-B supports stepwise refinement to allow each requirement to be introduced at the most appropriate stage in the development in order to manage complexity. UML-B supports refinement and, therefore, we also introduce an approach that allows to divide and layer OntoGraf diagrams into a number of layers that can be introduced as refinement in the UML-B diagrams.
Full PDF Version: 
Under Review