Modelling and analysis of the AMBA bus using CSP and B

Abstract

In this paper, we present a formal model and analysis of the Advanced Microcontroller Bus Architecture (AMBA) Advanced High-performance Bus (AHB). The model is given in CSP||B-an integration of the process algebra CSP and the state-based formalism B. We describe the theory behind the integration of CSP and B, and present the model in this theory. Analysis is performed using the model-checker ProB. The contribution of this paper may be summarized as follows: presentation of a formal model of the AMBA AHB protocol such that it may be used for analysis of co-design systems incorporating the bus, an evaluation of the integration of CSP and B in the production of such a model, and a demonstration and evaluation of ProB in performing this analysis. © 2009 John Wiley & Sons, Ltd.