Practical Techniques for the Design, Specification, Verification, and Implementation of Concurrent Systems

在过去的十年里，研究人员开发了一些工具，这些工具为将形式化方法应用于并发软件系统的设计和分析提供了自动化支持。原则上，这些工具允许系统设计人员利用正式的系统验证技术，而不需要他们了解基本数学理论的所有细节。然而，在实践中，这些工具的影响有限，因为它们可以处理的问题规模相对较小，而且它们缺乏对更传统的软件开发方法的支持，例如结构化设计技术、模拟和调试。本研究旨在将已有的并发系统自动化形式化技术的适用性扩展到实际规模和复杂性的问题。重点放在两个广泛的问题上：(1)提高现有方法的效率和可伸缩性；(2)通过将现有技术与更传统的软件开发方法相结合来增强现有技术的可用性。更具体地说，它寻求开发先进的状态空间管理技术，用于对照以模式u演算表示的逻辑属性来检查系统规范，以及用于以图形方式为未能满足其逻辑规范的系统传递诊断信息的技术。这项研究的影响正在通过分析几个现实生活中的应用程序来评估，例如滑动窗口通信协议和分布式共享内存的高速缓存一致性协议。这项研究建立在研究人员先前在并发工厂上所做的工作之上，该工厂是一个用于规范、模拟、验证和实现并发系统的集成工具集。*_

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. *** _