| HAL-Inria | Publications, software ... of Inria's scientists |
Reports
Generic Expression in B of the Influence/Reaction Model: Specifying and Verifying Situated Multi-Agent Systems
Abstract : This paper addresses the formal specification and verification of situated multi-agent systems that can be formulated within the influence-reaction model as proposed in 1996 by Ferber & Muller. In this framework our objective is to prove the correctness of reactive multi-agent systems with respect to a certain formal specification or property, using formal methods. This is an important step to bring multi-agent systems to high quality standards as required for critical applications encountered in domains such as transport systems. A generic B writing of systems instantiating the influence reaction model is proposed, using patterns of specification. An illustration is then presented on the formal specification of a system operating electrical vehicles under precise automatic control at close spacings 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.
Cited literature [22 references]
https://hal.inria.fr/inria-00173876
Contributor : Alexis Scheuer <>
Submitted on : Wednesday, September 26, 2007 - 9:29:11 AM
Last modification on : Thursday, March 4, 2021 - 3:12:16 PM
Long-term archiving on: : Friday, November 25, 2016 - 5:34:18 PM
Contributor : Alexis Scheuer <>
Submitted on : Wednesday, September 26, 2007 - 9:29:11 AM
Last modification on : Thursday, March 4, 2021 - 3:12:16 PM
Long-term archiving on: : Friday, November 25, 2016 - 5:34:18 PM
Files
SimoninEtalRR07.pdf
Files produced by the author(s)