Specifying in B the Influence/Reaction Model to Study Situated MAS: Application to vehicles platooning

Autor: Simonin, Olivier, Lanoix, Arnaud, Scheuer, Alexis, Charpillet, François
Přispěvatelé: Autonomous intelligent machine (MAIA), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Nantes Atlantique (LINA), Mines Nantes (Mines Nantes)-Université de Nantes (UN)-Centre National de la Recherche Scientifique (CNRS), Lanoix, Arnaud
Jazyk: angličtina
Rok vydání: 2011
Předmět:
Zdroj: V2CS : First International workshop on Verification and Validation of multi-agent models for complex systems
V2CS : First International workshop on Verification and Validation of multi-agent models for complex systems, Nov 2011, France. 15 p
Popis: International audience; This paper addresses the formal specification and verification of situated Multi-Agent Systems (MAS) that can be formulated within the Influence/Reaction model as proposed in 1996 by Ferber \& Muller. In this model, our objective is to prove the correctness of reactive MAS with respect to a certain formal specification or property, using formal methods. This is an important step to bring MAS to high quality standards as required for critical applications encountered in domains such as transport systems. A generic B representation of systems instantiating the Influence/Reaction model is proposed, using patterns of specification. We illustrate our approach with a MAS to control unmanned land vehicles to form a platoon. The papers ends with considerations about further improvements of the framework, involving simulation and study of the properties of the system.
Databáze: OpenAIRE
Externí odkaz: