Modeling ODP Policies by using event-B
Hafid Belhaj, Mohamed Bouhdadi, Elhajji Said · 2010
The Reference Model for Open Distributed Processing (RM-ODP) defines a framework for the development of Open Distributed Processing (ODP) systems in terms of five viewpoints: information, enterprise, computational, technology and engineering. Each viewpoint language defines concepts and rules for specifying ODP systems from the corresponding viewpoint. The enterprise viewpoint focuses on the roles and policies on the enterprise that the system is meant to support. The use of formal methods in the design process of ODP systems is explicitly required. Formal notations provide precise and unambiguous system specifications. An important point to take into account is the incorporation of the many proofs which have to be performed in order to be sure that the final system will be indeed “correct by construction”. The Event-B method is being defined as a formal notation. In this paper, we explore the benefits provided by using the proof construction approach to specify open distributed System in the enterprise viewpoint focusing on the specification of actions and the behavioral policies conditioning them.