Premium
Modelling and analysis of the AMBA bus using CSP and B
Author(s) -
McEwan Alistair A.,
Schneider Steve
Publication year - 2010
Publication title -
concurrency and computation: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.309
H-Index - 67
eISSN - 1532-0634
pISSN - 1532-0626
DOI - 10.1002/cpe.1432
Subject(s) - computer science , formalism (music) , process calculus , embedded system , formal methods , protocol (science) , programming language , computer architecture , medicine , art , musical , alternative medicine , pathology , visual arts
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.