Last year (1997) marked the 20th anniversary of the introduction of Temporal Logic (TL) into Computer Science as a language proposed for the specification and verification of Reactive Systems.
The talk will present a personal view of the main contributions and achievements of TL over the last two decades, emphasizing the recent increase of acceptance and adoption of the temporal methodology by industry, and the extensions of the formalism to deal with real-time and hybrid systems. We will then proceed to identify future challenges and directions that may extend the applicability of TL to wider classes of systems and the treatment of ever larger designs.
We start by identifying the class of reactive systems for whose specification and verification TL has proved to be a most natural and effective language. These are systems whose role is to maintain an ongoing interaction with their environment, rather than produce a final result upon termination. Most embedded systems which control an external physical environment belong to this important class. Such systems must be specified and analyzed in terms of their behaviors.
To model the behavior of reactive systems, we propose the computational model of a Fair Transition System (FTS) which, using two notions of fairness, captures the qualitative (non-quantitative) essence of reactive systems in an abstract and robust way. This model focuses on the precedence relation between events occurring in the behavior of a reactive system.
Temporal Logic is introduced as a language for writing predicates over sequences of states (equivalently actions), thus specifying a subset of all possible behaviors as being ``acceptable'', and providing an abstract specification of a reactive systems. We discuss two prevalent styles of reactive specification: The Requirement List style, and the Reference Model style. It is shown that TL is adequate for both specification styles.
Two approaches have been extensively employed for verifying that a given FTS satisfies a temporal specification: the Deductive and the Explorative. The deductive approach employs deductive rules and auxiliary constructs provided by the user, to reduce the temporal verification problem into a set of first-order implications that can be proven by available theorem-proving systems, such as PVS, SteP, or HOL.
The explorative approach (e.g., SMV, FormalCheck) is based on a traversal of a graph consisting of all the reachable states of the given FTS, and checking which states satisfy each sub-formula of the specification. The development of the method of Symbolic Model Checking transformed the explorative approach into the method most widely used in industry. The main advantage of the explorative approach is that it is algorithmic and requires no user intervention. The main disadvantage is that it is restricted to finite-state systems.
Important extensions of the temporal methodology allow it to deal with real-time systems, where precise time bounds are specified and need to be verified. An even more challenging extension is the consideration of HYBRID SYSTEMS which provides a single verifiable model for system combining discrete elements, such as a digital controller, with a continuous environment such as a physical plant. This fast-evolving interdisciplinary field combines insights and methods from both Control Theory and Computer Science.
In the last part of the talk, we will outline the main challenges of the field, which are to make the temporal methodology applicable to industrial-size systems. Certain promising avenues towards this goal will be discussed and evaluated.