Promela |
Omissions |
realtime(7) |
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.
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).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |