A New Extensible Framework for Multi-Agent System Verification
Franco Raimondi, Middlesex University London
Date and time: Thursday 7th March 2013 at 16:00
Location: G29, Mech Eng
Host: Mirco Musolesi
Recently, there has been a proliferation of tools and languages for modeling multi-agent systems (MAS). Verification tools, correspondingly, have been developed to check properties of these systems. Most MAS verification tools, however, have their own input language and often specialize in one verification technology, or only support checking a specific type of property.
In this talk I present an extensible framework that leverages mainstream verification tools to successfully reason about various types of properties. The Brahms agent modeling language is used to demonstrate the effectiveness of the approach (Brahms is used to model real instances of interactions between pilots, air-traffic controllers, and automated systems such as the NASA autopilot). The framework takes as input a Brahms model along with a Java implementation of its semantics and explores all possible behaviors of the model. The model is then verified using mainstream model checkers, including PRISM, SPIN, and NuSMV. (This is work in collaboration with Neha Rungta @NASA Ames and Richard Stocker @Liverpool, based on a paper accepted at AAMAS 2013)