Temporal Verification and Development of Reactive Programs

时态逻辑是一种有用的、强大的形式主义，用于描述、分析和开发一大类系统，即反应性系统。这类系统包括并发和实时程序、过程控制和嵌入式程序、硬件设备以及其他其作用是与其环境保持持续交互的系统。时态逻辑在通信协议的设计和验证、硬件设计和分析、并发程序综合和数据库分析等领域有着广阔的应用前景。本研究旨在使时间形式主义成为一种实用的工具。主要目标是为反应系统的规范、验证、开发和自动综合建立统一的时序逻辑方法，并建立一个将为这些活动提供计算机支持的实验系统。为了达到这些目标，研究内容包括：时态逻辑规范的表达能力和方便性，以及通过过去的算子和状态变量的量化等扩展可能的改进；时态逻辑与自动机等变迁系统的结合；时态规范的组合性，作为通过分解和精化进行系统开发的基础。

Temporal logic is a useful, powerful formalism for the specification,analysis, and development of a large class of systems, reactive systems. This class of systems includes concurrent and real- time programs, process control and embedded programs, hardware devices, and other systems whose role is to maintain a continuous interaction with their environment. Promising applications of temporal logic have been reported in diverse areas such as the design and verification of communication protocols, hardware design and analysis, synthesis of concurrent programs, and database analysis. This research is aimed at making the temporal formalism into a practical tool. The primary goals are to establish a uniform temporal- logic methodology for the specification, verification, development, and automatic synthesis of reactive systems, and to construct an experimental system that will provide computerized support for these activities. To attain these goals the investigation includes: the expressive power and convenience of specification by temporal logic, and its possible improvements by extensions such as past operators and quantification over state-variables; Combination of temporal logic with transition systems, such as automata; Compositionality of temporal specifications as a basis for systematic development by decomposition and refinement.