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.