The goal of this collaboration between the PI and Bernhard Steffan of the University of Passau is to study issues related to modeling and verification of distributed systems. Two specific threads of research will be pursued. The first involves the incorporation of notions of action priority into the semantic foundations of concurrency and an exploration of its practical impact on reasoning about system designs. The second is devoted to the design and implementation of an open tool architecture that will facilitate the development of new and improved verification tools. The results of this research will be new and useful extensions to system design methods and a framework for improved tool support for system designers.
