Skip to main content
main-content

Über dieses Buch

Reactive systems are computing systems which are interactive, such as real-time systems, operating systems, concurrent systems, control systems, etc. They are among the most difficult computing systems to program. Temporal logic is a formal tool/language which yields excellent results in specifying reactive systems. This volume, the first of two, subtitled Specification, has a self-contained introduction to temporal logic and, more important, an introduction to the computational model for reactive programs, developed by Zohar Manna and Amir Pnueli of Stanford University and the Weizmann Institute of Science, Israel, respectively.

Inhaltsverzeichnis

Frontmatter

Models of Concurrency

Frontmatter

Chapter 1. Basic Models

Abstract
Programs and the systems they control can be conceptually partitioned into transformational and reactive programs and systems.
Zohar Manna, Amir Pnueli

Chapter 2. Modeling Real Concurrency

Abstract
An essential element of the generic model used in this book is that concurrency is represented byinterleaving.This means that, according to the formal model, two parallel processes never execute their statements at precisely the same instant, but take turns in executing atomic transitions. Formally, when one of them executes an atomic transition, the other is inactive. This model of computation is very convenient for the formalization, analysis, and manipulation of concurrent programs.
Zohar Manna, Amir Pnueli

Specifications

Frontmatter

Chapter 3. Temporal Logic

Abstract
In the preceding chapters, we introduced the concept of a fair transition system as a model for reactive systems. Following the general definition, we presented several concrete languages for concurrent systems and showed how they can all be cast in the general framework of transition systems.
Zohar Manna, Amir Pnueli

Chapter 4. Properties of Programs

Abstract
In this chapter we will illustrate the use of temporal logic for specifying properties of programs. To introduce some structure in the extensive set of program properties, we define a hierarchy of the properties expressible by temporal logic, which is based on the types of formulas used to express the properties. We consider, in turn, each class in the hierarchy of temporal properties and present examples of concrete properties that fall into this class.
Zohar Manna, Amir Pnueli

Backmatter

Weitere Informationen