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:
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.
This research was sponsored by AFOSR (FA9550-06-1-0058) from 2006 - 2008.