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