Event-B specification of transportation system in dynamic environment: Study of urban public Transportation system

Formal reasoning is needed to ensure system correctness and structure their development. Event-B is a formal method with tool support allowing a stepwise development of reactive distributed systems. We propose using Event-B to helpful the specification and the safe development of Multi-Agent System. Agent technology is a software paradigm that permits to implement large and complex distributed applications. In order to assist the development of multi-agent systems, agent-oriented methodologies (AOM) have been created in the last years to support modeling more and more complex applications in many different domains. But this specification remains abstract and it necessity a formal method in order to obtain a consolidated specification. In this article, we mainly report our experience with the Event-B stepwise in order to specify and validate our new agent-oriented meta-model (Platooning Meta-Model) that allow the analyst to model and specify any transportation system as a multi-agent system in a dynamic environment. This article also aims at serving as a guide for the development of other MAS, taking agents specific features and the environment properties into account.