Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles

Arnaud Lanoix (1)

1 DEDALE - Development of specifications

Situated Multi-Agents Systems (MAS), and other Agent-based systems, are often complex. Formal reasoning is needed to ensuring their correctness and structuring their development. Event-B is a formal method with tool support allowing a stepwise development of reactive distributed systems. MAS being a subclass of such systems, we propose using Event-B to helpful their specification and their safe development. In this article, we mainly report our experience with the Even-B stepwise development of a situated MAS which study the displacement of vehicles in a convoy. This article aims also at serving as a guide for the development of other MAS, taking agents-specific features into account.

Domaines: Génie logiciel [cs.SE]

Arnaud Lanoix. Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles. 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2008), Jun 2008, France. 8 p. ⟨hal-00260577⟩