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

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

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