Third International Conference on Computing and Wireless Communication Systems, ICCWCS 2019, April 24-25, 2019, Faculty of Sciences, Ibn Tofaïl University -Kénitra- Morocco

Research Article

Reference Model of Open Distributed Processing Basic Modelling Concepts in Event-B

Download89 downloads
  • @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={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
Abdessamad jarrar1,*, Nawfal FERFRA2, Taoufiq Gadi3, Youssef Balouki3
  • 1: PhD student
  • 2: CMR The Moroccan Pension Fund
  • 3: Professor at University Hassan First
*Contact email: abdessamad.jarrar@gmail.com

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.