Verifying part of the ACCESS.bus protocol using PVS
Jozef Hooman
Appeared in: Proceedings 15th Conference on the Foundations of Software
Technology and Theoretical Computer Science, LNCS 1026, Springer-Verlag,
pages 96-110, 1995.
ABSTRACT
Based on a compositional framework for the formal specification
of distributed real-time systems, we present a method for
protocol verification.
The application of this formal method to large realistic
systems clearly requires some form of mechanical support.
For instance, one would like to check proofs mechanically,
to construct proofs interactively,
and to discharge simple verification conditions
automatically.
Therefore our method is supported by the interactive proof checker
PVS (Prototype Verification System).
To illustrate the method and the use of PVS during protocol verification,
we consider part of the ACCESS.bus protocol.
ACCESS.bus is used for the communication between a computer host
and its peripheral devices, such as keyboards, mice, joysticks, modems,
monitors and printers.
The bus supports dynamic reconfiguration while the system is operating.
We specify and verify a safety property and a real-time progress
property of this industrial example.
Postscript