Formal Reasoning about Reactive Systems

人们越来越需要有效的形式化方法来构建正确可靠的计算机程序。在并发的、分布式的、实时的，或者更普遍的反应性系统的情况下，这种需求变得尤为重要。这样的系统通常涉及许多微妙的方面，例如不同的、通常在地理上分散的组件的并行操作，以及正在进行的、理想的非终止计算，其中每个组件重复与相邻组件交互，以实现全局目标或保持全局不变性。许多安全关键的实际应用程序可以算在反应系统中。例子包括：计算机操作系统、计算机网络通信协议、空中交通管制系统、机载航空电子控制系统以及自动银行网络。在这项研究中，对这种反应性系统进行推理的方法以时间逻辑的使用为中心，时间逻辑是一种可用于规范、验证、设计和合成反应性系统的形式化方法。本研究探讨在何种程度上有效的自动化时间推理的反应系统是可能的。主要关注以下几个方面：解决状态爆炸问题，对许多同质过程的推理，实时推理和反应系统的综合。

There is a growing need for effective formal methods of constructing correct and reliable computer programs. This need becomes especially crucial in the case of concurrent,distributed, real-time, or, more generally, reactive systems. Such systems typically involve a number of delicate and subtle aspects such as parallel operation of distinct, often geographically dispersed components, and ongoing, ideally nonterminating computation where each component repeatedly interacts with neighboring components in order to achieve a global goal or maintain a global invariant. Many safety critical real-world applications programs can be counted among the reactive systems. Examples include: computer operating systems, computer network communication protocols, air traffic control systems, on-board avionics control systems, as well as automated banking networks. The approach taken in this research to reasoning about such reactive systems centers around the use of Temporal Logic, a formalism that can be used for specification, verification, design, and synthesis of reactive systems. This research investigates to what extent efficient automation of temporal reasoning about reactive systems is possible. Considerable attention is devoted to the following particular aspects: attacking the state explosion problem, reasoning about many homogenous processes, real-time reasoning, and synthesis of reactive systems.