Modelling and analysis of the AMBA bus using CSP and B

Abstract. In this paper, we present a formal model and analysis of the AMBA Ad-vanced High-performance Bus (AHB) on-chip bus. 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. We demonstrate how the model is developed from the informal ARM specification of the bus. Analysis is performed us-ing the model-checker ProB. The contribution of this paper may be summarised as follows: presentation of work in progress towards a formal model of the AMBA AHB protocol such that it may be used for inclusion in, and 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 the ProB tool in performin