Modelling and analysis of the AMBA bus using CSP and B
Alistair A. McEwan, Steve A. Schneider · Concurrency and Computation Practice and Experience · 2009
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. Copyright © 2009 John Wiley & Sons, Ltd.