Methodologies for the Automatic Verification of Concurrent Systems

尽管对并行计算系统进行了十多年的研究，但由于同时执行的组件可能存在微妙的相互作用，这类系统的开发仍然是一项困难和容易出错的工作。确保此类系统正确运行的一种方法是正式验证它们；然而，这可能是一项极其复杂的任务，即使是自动化工具的开发也不允许非常大的系统被证明是正确的。使用进程代数的框架，这个项目的广泛目标是开发自动化技术，使大型并发系统的验证成为可能。该项目将沿着三条线进行。将开发利用并发系统的结构及其规格的方法，以将核查过程减少为一组更易于管理的子问题，这些子问题可利用现有技术加以解决。支持这些方法的自动化工具将构建在现有工具--并发工作台之上，该工具为建议的技术提供所需的基本支持。这些方法和相关工具的效用将通过将它们应用于现有“现实世界”通信协议的核查来进行评估。

Despite more than a decade of research into parallel computing systems, the development of such systems remains a difficult and error-prone undertaking, owing to the subtle interactions in which simultaneously executing components may engage. One way to ensure that such systems behave correctly is to verify them formally; this, however, can be an extremely complex task, and even the development of automated tools has not permitted very large systems to be proved correct. Using the framework of process algebra, the broad goal of this project is to develop automated techniques that enable the verification of large concurrent systems. The project will work along three lines. Methodologies will be developed that exploit the structure of concurrent systems and their specifications to reduce the verification process to a collection of more manageable subproblems that may be solved using existing techniques. Automated tools that support these methodologies will be built on top of an existing tool, the Concurrency Workbench, which provides the basic support needed for the proposed techniques. The utility of the methodologies and associated tools will be evaluated by applying them to the verification of existing "real world" communications protocols.