Validation and analysis of the future bus arbitration protocol: a case study

Abstract

In this paper, we use perfectly synchronous languages such as Esterel, for modelling Futurebus arbitration protocol. We show that the perfect synchrony aids in the formalization, testing, validating and verifying the protocol. We discuss solutions to the above protocol and show that properties such as mutual exclusion and deadlock-freedom can be established formally. Further, we show how the simulators can be used for testing and validation and can verify an instantiation of the protocol through algebraic tools such as auto/autograph.