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. Revised version of McEwan AA, Schneider S. Modelling and analysis of the AMBA bus in CSP and B. In McEwan AA, Schneider S, Ifill W, Welch PH (eds). Communicating Process Architectures 2007. IOS Press: Amsterdam. Published with permission from IOS Press.