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.