This section describes the important features of real-time systems. The following problems are also posed: the modelling problem, the verification problem, the design development problem and the controller synthesis problem. These are some of the main problems that theorists hope to tackle with formal methods.
An algorithm is usually represented as a program. Correctness of the algorithm means that the program satisfies some desired specification (or property). Therefore, in standard program verification, three concepts are needed. A programming language is needed for representing algorithms, a specification language for expressing properties, and a satisfaction relation (or proof system) for verifying the correctness of the algorithm. An important subjective issue revolves around the choice of syntax for the programming and specification languages — does the syntax simplify the expression of algorithms and specifications, or does it get in the way of the designer.
To properly develop the concepts mentioned above, some additional notions must be introduced. A formal semantics must be provided so that the behaviour of the program and the meaning of the specifications are clearly defined. The proof system must be shown to be sound with respect to the semantics, so that only those programs whose behaviours satisfy the specification can be proven correct. An unsound proof system is dangerous because it can be used to prove anything (papers on the assignment axiom for arrays were, for years, filled with errors). Furthermore, it is useful if the proof system is complete so that every correct program can be verified for correctness in the proof system. Other issues such as the expressiveness of the languages and the complexity of decision procedures must be explored.
An algorithm usually takes some data as input, performs a computation and outputs the result of the computation to the user. For real-time programs, the situation is more complex. The environment in which the program operates can no longer be ignored, because of the intensive non-terminating interaction of the program with its environment. Such systems are often called embedded systems, discrete event dynamic systems, reactive systems, or process control systems. We shall refer to all of these as ``real-time systems''.
Ordinary programming languages are not expressive enough to represent the complex features of real-time systems such as concurrency, nondeterminism, synchronization between processes and real-time constraints on the events of such systems. Programming languages must therefore be extended if they are to deal with real-time systems. A model of the intended real-time notions is therefore needed.
A model is a representation, often in mathematical terms, of the important features of the system that is being studied. A common modelling technique is to define the state of the system (a ``snapshot'' at an instant in time of all the variables defining the system). A state may persist for some period of time, after which there is some change to a new state (as real-time systems are dynamic). Such a state change is referred to as an event or a transition. The model may be used to simulate possible behaviours of the system which helps the designer understand the system better. A simulation of the system is a sequence of states and events capturing the behaviour of the system. A simulation may show the presence of bugs in the system, but never their absence [23]. Analysis of the system behaviour must be undertaken to show the correctness of the system. The system is correct provided that its behaviour satisfies the associated specification.
The terms ``model'' and ``specification'' are often used interchangeably. In this survey, a model is a description of the system, perhaps in great detail, or perhaps at a more abstract level. A specification is the list of requirements that the system must ideally satisfy. A model describes how the system actually behaves. A specification prescribes how we would like it to behave.
What are the most important features of a real-time system? The Oxford Dictionary of Computing defines a real-time system as follows:
[A real-time system is] any system in which the time at which the output is produced is significant. This is usually because the input corresponds to some movement in the physical world, and the output has to relate to that same movement. The lag from input time to output time must be sufficiently small for acceptable timeliness.
The IEEE Standard Dictionary of Electrical and Electronic Terms (Wiley 1978) gives the following definition:
Real-Time: (A) Pertaining to the actual time during which a physical process transpires. (B) Pertaining to the performance of a computation during the actual time that the related physical process transpires in order that results of the computation can be used in guiding the physical process.
In software engineering, the term ``real-time system'' usually refers to the software or programming code (called the controller in this survey). The lag time from input to output in the controller must be sufficiently small. However, there is implicitly always another object that is associated with the controller. That object is the physical world or environment in which the controller finds itself. Since the environment is always implicitly there, let us give it a name and call it the plant. Then we can refer to the plant and perhaps even reason about it. In fact, the lag time or response time of the controller is determined by the physical nature of the processes in the plant. The primary goal of the designer is to ensure the correct behaviour of the plant. This is achieved by designing a controller that will interact and control the plant. We may draw an automatic control diagram that is familiar to control engineers:
It is the task of the controller to ensure that unsatisfactory behaviour in the plant is eliminated. The diagram above indicates the role that feedback plays in the controller. Feedback restores equilibrium after disruptions caused by disturbances to the plant. After measuring the current state of the plant the controller can take corrective action by issuing appropriate control commands.
There is usually much more freedom in the design of the controller than in that of the plant. In fact, the controller is often implemented by real-time software precisely so that the logic of the controller, or the computation that it performs, can easily be changed if necessary. As a result, the design of a real-time system differs from straight programming (e.g. coding an algorithm) in two important respects:
The design formalism must be flexible enough to represent the plant as an integral part of the complete system. Unsatisfactory plant behaviour can then be examined, and the effect of different control policies on the plant can be evaluated. Potential failures of the plant must be represented in the plant model so that the controller can be checked to see that it functions correctly. A model of the plant will enable the designer to extract the lag and real-time response times that the controller must implement. Furthermore, a deterministic formalism developed for a real-time programming language (to guarantee predictable behaviour), may be unsuitable for representing nondeterministic and asynchronous event driven plant behavior.
Consider the following robot example2. The system under development (SUD) is a robot arm together with position sensors, a force sensor, a camera, a tactile sensor, a gripper, a joystick and keyboard for input, and a computer to control the various parts. Formally, we may write
The model of the plant will have to represent certain timing constraints. The camera works at 30 Hz, and the force sensor at 400Hz. The robot and position sensors work at 1000Hz, the joystick at 25Hz, and the tactile sensor at 120Hz.
The required specifications are: design a controller that will enable a user to manipulate the arm to perform various tasks at certain speeds, e.g. welding a part to an auto on the assembly line. The sensor measurements must be scanned at the correct rate. The actuators must be activated at the correct time. If an unfamiliar obstacle is encountered stop the arm movement within one second.
The specification S of required behaviour so far only refers to elements of the plant such as the arm, the sensors and actuators. The controller must still be designed, and so its constituent parts cannot yet be referred to in the top level specification.
Having specified as precisely as possible the plant, and the specification S that it must satisfy, the controller must now be designed. It was necessary to structure the description of the plant with the parallel composition operator. So too, it is often also necessary to structure the controller description.
For example, it is possible that only some of the sensors will be used at any one time. A logical way to separate the control functions is by having one task supervise the control signals to the robot and another task read the camera. Other distinct tasks can read the position and force sensors. If only the force sensor is needed for a particular task, and not the camera, then it is simply a matter of starting up the appropriate tasks without the need to change any code.
Without concurrency the software must be constructed as a single control loop called a cyclic executive. Such a large sequential program with multiple conditional flags such as ``if (using camera) do action'' is difficult to design robustly because of the different time frames and functions that must be accommodated. The structure of this loop cannot retain the logical distinction between controller modules. It is difficult to ensure that the executive synchronizes in a timely fashion with the plant processes, without the explicit notion of concurrent tasks in the controller software.
In a concurrent controller, each time frame is handled by a different task. The frequency of each task can be specified separately, and the burden of deciding what to run when is placed on the operating system scheduler. Even if the timing changes, there is no need to reprogram the controller. The real-time operating system is designed so as to be capable of adapting to the new requirements. If a large sequential program is used, the entire program would have to be restructured to satisfy the new timing requirements.
The use of concurrency is not without cost. There must be a run time support system to manage execution of controller tasks or processes. Such run time schedulers are often not considered in formal verification methods, but should be for a complete treatment of all system issues. Scheduling is treated as one discipline and verification as a different one. Methods that treat, in a unified framework, all aspects of verification and scheduling have not been sufficiently developed.
There is one part of the design process that is informal and intuitive. When the real world (e.g. of valves, pumps, vehicles, and robot arms) is translated into a formal mathematical model plant (e.g. of states, events and time bounds), there is no guarantee that the mathematical model properly represents the actual objects to be controlled. Similarly, there is no guarantee that the model controller is an accurate representation of all important facets of the actually implemented software (together with the hardware, CPU and run time system). This translation of real world objects into mathematical entities is by its very nature informal and intuitive.
As more experience is gained with a particular formalism, and actual designs based on the formal methods are experimentally checked in the field, so the formalism will gain more credibility. This is no different from the methods used in related disciplines. For example, a civil engineer will model the real world of bridges, beams and winds using the formal techniques of Newtonian physics. As more bridges are built and actually succeed in practice, so the Newtonian models gain credibility.
In certain cases, the pure Newtonian model must be adjusted with ``safety factors'' to account for the approximate nature of the models used. It is not clear what the software equivalent of safety factors is.
The fact that one part of the design procedure remains informal and experimental does not in any way detract from the need to use formal design procedures in the rest of the design. Just as the civil engineer uses formal Newtonian models for bridge building, and thereby increases confidence in the design, so too the designer of software uses formal methods to increase confidence in the correctness of the real-time system design. A proof of correctness is always relative to the formal models and specifications provided.