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.


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.