Modelling and analysis of the AMBA bus using CSP and B
Tools
Tools
Tools
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]](http://epubs.surrey.ac.uk/style/images/fileicons/text.png)
|
Text
ccpe09b.pdf Available under License : See the attached licence file. Download (318kB) |
|
|
Text (licence)
licence.txt Download (1kB) |
Official URL: http://dx.doi.org/10.1002/cpe.1432
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 : |
|
|||||||||
| 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 : | 31 Oct 2017 14:09 | |||||||||
| URI: | http://epubs.surrey.ac.uk/id/eprint/7243 |
Actions (login required)
 |
View Item |
Downloads
Downloads per month over past year