Modelling and analysis of the AMBA bus using CSP and B
McEwan, AA and Schneider, S (2010) Modelling and analysis of the AMBA bus using CSP and B Concurrency and Computation: Practise and Experience, 22 (8). pp. 949-964.
Available under License : See the attached licence file.
Plain Text (licence)
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 parallel to 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 (C) 2009 John Wiley & Sons, Ltd.
|Divisions :||Faculty of Engineering and Physical Sciences > Computing Science|
|Date :||10 June 2010|
|Identification Number :||10.1002/cpe.1432|
|Uncontrolled Keywords :||CSPB parallel to B, AMBA, formal modelling, ProB, co-design|
|Additional Information :||This is the peer reviewed version of the following article: McEwan, AA and Schneider, S (2010) Modelling and analysis of the AMBA bus using CSP and B. Concurrency and Computation: Practise and Experience, 22 (8). 949 - 964, which has been published in final form at http://dx.doi.org/10.1002/cpe.1432. This article may be used for non-commercial purposes in accordance with Wiley Terms and Conditions for Self-Archiving.|
|Depositing User :||Symplectic Elements|
|Date Deposited :||02 Dec 2015 11:00|
|Last Modified :||02 Dec 2015 11:00|
Actions (login required)
Downloads per month over past year