Formal Modelling of Domain Constraints in Event-B

When designing a hardware or a software system, the integration of domain constraints becomes a determining factor to ensure a great match with the system requirements. This domain knowledge is most often modelled using ontologies that allow to express the domain data properties. In this paper, we propose an approach to integrate domain ontologies into a system development process based on Event-B. It consists to annotate Event-B models using the ontology concepts, this assumes a formalization of the domain ontology in the Event-B method. Therefore, we propose an extensible generic transformation approach which develops an Event-B specification based on an ontology described in an ontological language. The integration of the Event-B description of a domain ontology allows to constrain the system under design with the domain ontology and to validate domain properties.