The goal of PRiMO is to develop methods, techniques, and tools to allow developers to design and build highly adaptive distributed systems that are assured of meeting specific design goals.  Specifically, we will focus on ensuring that, at design time, system flexibility and robustness are measured and designers are given ample time and freedom to explore alternative designs.  To measure these parameters, we plan to use model checking.  In addition, we plan to explore many other types of verification at various stages of the development lifecycle.  Thus, the five central objects of the proposed research are to:

• Develop a model-driven software engineering methodology for the development of high-assurance, highly adaptive multiagent systems.
• Explore policy-based mechanisms for specifying application-specific properties and metrics for adaptive multiagent systems.
• Use model checking and other lightweight verification techniques to validate each step and transformation within our methodology and provide estimates of design parameters such as flexibility.
• Develop model/method-specific extensions (to include algorithms, types, expressions, and commands) to the Bogor model checker to provide robust, efficient verification capabilities.
• Develop an integrated set of tools to support our proposed software methodology and automated verification capabilities.

Background

Our approach is based on the emerging model-driven development (MDD) software engineering methodology that provides separations of concerns of the various aspects in software development by using integrated (abstract) system models to capture those aspects. One main benefit of this approach is that concerns are exposed only at the appropriate levels of abstraction, thus allowing developers to better concentrate on issues relevant to their development stages. For example, in a design level of a distributed multiagent system, one does not want to concern about network communication. Instead, one might focus on the capabilities of the agents and the tasks that the agents should achieve.

A disadvantage of the MDD approach is that we must have the “right” formalisms to describe the models of the systems. In our case, we propose to leverage the organization model in the Multiagent Software Engineering (MaSE) methodology that we developed over the past several years as our basis formalism. In addition, we propose to develop models to capture different concerns in multiagent system and their sound refinements, accompanied by strong assurance techniques by leveraging our previous work in the Bogor software model checking framework.

Sponsor

This research was sponsored by AFOSR (FA9550-06-1-0058) from 2006 - 2008.