A Unified Framework for Verification and Complexity Analysis of Real-Time and Distributed Systems

这个项目的目标是定义一个通用的形式化模型，用于实时和分布式系统的推理，并通过将其用于各种目的来确定其价值。已经为这类系统提出了许多模型；该项目的独特之处在于它试图定义可用于多种不同目的的单一模型。这种模型的用途包括：(1)证明关于实时和分布式系统能力的基本结果。这些结果包括复杂性的上下界结果(时间、空间和通信复杂性)和不可能性结果：(2)使用适当的编程语言描述真实系统；(3)指定允许的系统行为；(4)(手动或机器)验证算法和系统的正确性。有不同的验证方式，其中断言、代数和时序逻辑方法可能是最重要的；(5)分析系统性能。传统上，这些领域中的每个领域的研究都是基于专门为该领域设计的语义模型。相比之下，该项目旨在按照一个共同模式开展这些领域的工作。该项目特别侧重于实时和其他基于时间的系统(例如，通信系统和实时过程控制系统)。

The goal of this project is to define a general formal model for reasoning about real-time and distributed systems, and to establish its value by using it for a variety of purposes. Many models have been proposed for such systems; this project is unique in that it attempts to define a single model that can be used for many different purposes. The uses for such a model include: (1) proving fundamental results about the capabilities of real-time and distributed systems. These include upper and lower bound complexity results (for time, space and communication complexity) and impossibility results: (2) describing real systems, using appropriate programming languages; (3) specifying allowable system behavior; (4) verifying (by hand or by machine) the correctness of algorithms and systems. There are different styles of verification, of which assertional, algebraic and temporal logic methods are probably the most significant; and (5) analyzing system performance. Traditionally, research in each of these areas has been based on a semantic model designed specifically for that area. In contrast, this project aims to conduct work in these areas in terms of a common model. The project focuses particularly on real-time and other timing-based systems (e.g., communication systems and real-time process control systems).