Research Article
Reference Model of Open Distributed Processing Basic Modelling Concepts in Event-B
@INPROCEEDINGS{10.4108/eai.24-4-2019.2284096, author={Abdessamad jarrar and Nawfal FERFRA and Taoufiq Gadi and Youssef Balouki}, title={Reference Model of Open Distributed Processing Basic Modelling Concepts in Event-B}, proceedings={Proceedings of the Third International Conference on Computing and Wireless Communication Systems, ICCWCS 2019, April 24-25, 2019, Faculty of Sciences, Ibn Tofa\~{n}l University -K\^{e}nitra- Morocco}, publisher={EAI}, proceedings_a={ICCWCS}, year={2019}, month={5}, keywords={open distributed processing rm-odp formal methods event-b architecture semantic formalization}, doi={10.4108/eai.24-4-2019.2284096} }- Abdessamad jarrar
Nawfal FERFRA
Taoufiq Gadi
Youssef Balouki
Year: 2019
Reference Model of Open Distributed Processing Basic Modelling Concepts in Event-B
ICCWCS
EAI
DOI: 10.4108/eai.24-4-2019.2284096
Abstract
We present a set of recommendations to help engineers using the Event-B formal methods to specify the basic modelling concepts of the Reference Model of Open Distributed Processing (RM-ODP). This model is developed by the IUT and ISO in order to standarise the development of Open Distributed Processing (ODP). RM-ODP is criticized for inssuficient definition of the basic modeling concepts which limits the applicability of the model. Therefore, the IUT and ISO provide for users a sematic architecture formalization in several formal methods (LOTOS, ACT ONE, SDL-92, Z, and ESTELLE). However, these formal methods are very basic and suffer from the lack of predefined mathematical operators and also some of them are very poor in term of specification techniques. These issues encourage us to develop our recommendations for specifying and developing the ODP using a more sophisticated method called Event-B. This formal methods is very rich in term of predifined mathematical operator and provides sophisticated techniques that can be used during the specification process. Additionaly, Event-B provide a set of verification proofs that highly guarentee the absence of bugs.