Over the past decade, researchers have developed tools that offer automated support for applying formal methods to the design and analysis of concurrent software systems. In principle, these tools allow system designers to utilize formal system verification techniques without requiring them to know all the details of the underlying mathematical theories. In practice, however, the impact of the tools has been limited because of the relatively small scale of the problems they can handle and because of their lack of support for more traditional development methods for software, such as structured design techniques, simulation, and debugging. This research project aims at extending the applicability of existing automated formal techniques for concurrent systems to problems of real-life scale and complexity. The focus is on two broad issues: (1) increasing the efficiency and scalabity of existing approaches; and (2) enhancing the usability of existing techniques by integrating them with more traditional software development methods. More specifically, it seeks to develop advanced state-space management techniques for checking system specifications against logical properties expressed in the modal mu-calculus, and techniques for graphically conveying diagnostic information for systems that fail to meet their logical specifications. The impact of the research is being assessed by analyzing several real-life applications, such as sliding-window communications protocols and cache coherency protocols for distributed shared memory. This research builds on the investigators' prior work on the Concurrency Factory, an integrated toolset for specification, simulation, verification, and implementation of concurrent systems. *** _
