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

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

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