Methodologies for the Automatic Verification of Concurrent Systems

这个项目的目标涉及开发有限状态并发系统自动验证的实用方法，包括硬件设计、通信协议和软件需求规范。这类系统的设计、调试和维护是出了名的困难，这是由于并行性引起的组件之间微妙的、经常是意想不到的交互。克服这些问题的一个吸引人的方法是使用数学推理来确保系统按预期运行；这项研究的目的是通过开发合适的技术和相关的软件工具，使这种形式化的分析成为现实，使设计师能够在构建系统时分析他们的系统。拟议的工作将沿着以下方向发展：将研究更有效的算法，以确定并发系统的正确性；将研究能够分析比目前能够管理的更大系统的技术；将开发可用的图形和文本设计语言，并实施适当的工具；将开发和实现实时系统和系统相对可靠性的推理方法。＊＊＊

9402807 Cleaveland The goals of this project involve the development of practical approaches to the automatic verification of finite-state concurrent systems, including hardware designs, communications protocols, and software requirements specifications. Such systems are notoriously difficult to design, debug and maintain, owing to the subtle and often unanticipated interactions between components that parallelism induces. One appealing approach to overcoming these problems involves the use of mathematical reasoning to ensure that systems behave as intended; this research aims at making the use of such formal analysis practical by developing suitable techniques, and associated software tools, that enable designers to analyze their systems as they are building them. The proposed work would develop along the following lines: Research would undertaken into more efficient algorithms for determining the correctness of concurrent systems; techniques would investigated for enabling the analysis of larger systems than can currently be managed; he development of usable graphical and textual design languages would undertaken, and appropriate tools implemented; methods would develop and implement for reasoning about real-time systems and about the relative reliability of systems. ***