Methodologies for the Automatic Verification of Concurrent Systems

9402807明确本项目的目标包括开发自动验证有限状态并发系统的实用方法，包括硬件设计、通信协议和软件需求规范。众所周知，这种系统很难设计、调试和维护，这是因为并行性导致的组件之间微妙且经常是意想不到的交互。解决这些问题的一个吸引人的方法是使用数学推理来确保系统按预期运行；本研究的目的是通过开发适当的技术和相关的软件工具，使这种形式分析的使用变得实用，使设计人员能够在构建系统时分析他们的系统。拟议的工作将沿着以下方向发展：研究确定并发系统正确性的更有效的算法；研究能够分析比目前能够管理的更大的系统的技术；开发可用的图形和文字设计语言，并采用适当的工具；开发和实施关于实时系统和系统的相对可靠性的推理方法。***

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