University of Surrey

Test tubes in the lab Research in the ATI Dance Research

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.

[img]
Preview
PDF
ccpe09b.pdf
Available under License : See the attached licence file.

Download (318kB)
[img] Plain Text (licence)
licence.txt

Download (1kB)

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 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.

Item Type: Article
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
AuthorsEmailORCID
McEwan, AAUNSPECIFIEDUNSPECIFIED
Schneider, SUNSPECIFIEDUNSPECIFIED
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
URI: http://epubs.surrey.ac.uk/id/eprint/7243

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800