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.