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 (A OM) 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.