NAME
real-time - for relating properties to real time bounds.

DESCRIPTION
In vanilla Promela there is no mechanism for expressing properties of clocks or of time related properties or events. There are good algorithms for integrating real time constraints into the model checking process, but most attention has so far been given to real time verification problems in hardware circuit design, rather than real time verification of asynchronous software , which is the domain of the Spin model checker. The best known of these algorithms incur significant performance penalties compared with untimed verification. Each clock variable added to a model can increase the time and memory requirements of verification by an order of magnitude or more. Considering that one needs at least two or three such clock variables to define meaningful constraints seems to imply, for the time being, that a real time capability requires at least three to four orders of magnitude more time an memory than the verification of the same system without time constraints.

Not withstanding the above, real time verification would be a valuable addition to the model checking system. Several research problems remain to be solved before we can do so. This is not dramatic, because Spin verifications do already have a considerable scope. Note for instance that if a correctness property can be proven for an untimed Promela model, it is guaranteed to preserve its correctness under all possible real time constraints. The result is therefore more robust, it can be obtained more efficiently, and it encourages good design practice because in concurrent software it is often not desirable to link logical correctness issues with the real time performance of concurrent processes.

Some of the research issues that remain to be solved can be summarized as follows.

• Promela is a language for specifying asynchronous processes, i.e., software systems. For the definition of such as system we abstract from the behavior of the process scheduler, and from any assumption about the relative speed of execution of the various processes. These assumptions are safe, and the minimal assumptions required to allow us to construct proofs of correctness. The assumptions differ fundamentally from those that can be made for hardware systems, which are often driven by a single, known, clock, with relative speeds of execution precisely known. What often is just and safe in hardware verifications, therefore, is not necessarily just and safe for software verifications. Spin guarantees that all verification results remain valid independent of where and how processes are executed, time-shared on a single CPU, in true concurrency on a multi-processor, or with different processes running on CPUs of different and varying speeds. Two points are worth considering in this context: first, such a guarantee can no longer be given if real time constraints are introduced, and secondly, the known real time verification methods assume a true concurrency model, and exclude the more common method of concurrent process execution by time-sharing.
• It can be hard to define realistic time bounds for an abstract software system. Typically, too little can be known about the real time performance of an implementation to be able to rely on this in a verification of its critical correctness properties.
• The performance of verification suffers more substantially if we also allow for symbolic constraints. For instance, in Fisher's well-known mutual exclusion protocol example, one would like to prove that correctness is guaranteed provided only that one set of transitions always takes longer to execute than another set of transitions, irrespective of how long each interval lasts precisely. There are no efficient algorithms known at this time to handle such problems.

NOTES
There are several serious projects in progress to study the above problems and to explore sound real time extensions of Spin. Sooner or later Spin is expected to acquire a real time verification capability based on these studies.

SEE ALSO
probabilities(7).