for relating properties to real time bounds.
In vanilla Promela there is no mechanism for expressing
properties of clocks or of time related properties
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
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.,
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 how long each interval lasts precisely. There are no
efficient algorithms known at this time to handle such problems.
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.