Formal Modelling of Ontologies : An Event-B based Approach Using the Rodin Platform

Nowadays, it is well accepted that formal ontologies are commonly used as support for the axiomatisation of the knowledge describing a domain of interest. In particular, for domains in the engineering area where concepts are well mastered by the different stakeholders, ontologies play a major role for knowledge exchange and heterogeneity reduction. Meanwhile, we observe that defining a formal framework for integrating both ontologies represented by knowledge models and design models of particular systems did not draw the attention of many researchers in system engineering. Approaches like those of [3][4][5][7][9][12] supporting the integration of both ontologies and design models contribute to strengthen these design models by offering the capability to design models to borrow knowledge from ontologies, using a particular annotation relationship. As a consequence, the design models are enriched and strengthened with axioms, theorems or invariants issued from the used ontologies. This paper presents a summary of the work achieved in the context of the French ANR IMPEX research project. Ontologies are formalised as theories with axioms, theorems and reasoning rules. Event-B [1] has been chosen as the ground formal modelling technique for all our developments.