From GMoDS models to object-oriented specifications in Event-B

This paper represents a first attempt to express in Event-B the models of the GMoDS (The Goal Model for Dynamic Systems) methodology. GMoDS is a major result of the research related to Organization-Based Multiagent System Engineering methodology (O-MaSE), allowing to specify goals during requirements engineering process and then to use them throughout the system development and at runtime. We choose Event-B as a modelling language for specifying the GMoDS models for two reasons: (a) Event-B has the concept of proving correctness, which supports the accuracy of software development, and (b) its supporting tool, RODIN, is open-source, and it is used in many software industrial applications. Because Event-B is not object-oriented, and because several concepts used in GMoDS are related to object-orientation, we have included in the corresponding Event-B specifications the object-oriented concepts used in the GMoDS models, without changing the syntax and semantics of Event-B, and without using the UML-B tool.