Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B
Schneider, S and Treharne, H (2009) Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B In: 7th International Conference on Integrated Formal Methods, 2009-02-16 - 2009-02-19, Dusseldorf, GERMANY.
![]()
|
Text
ifm09.pdf - Accepted version Manuscript Available under License : See the attached licence file. Download (189kB) |
|
![]() |
Text (licence)
licence.txt Download (1kB) |
Abstract
This paper introduces action refinement in the context of CSP||B. Our motivation to include this notion of refinement within the CSP parallel to B framework is the desire to increase flexibility in the refinement process. We introduce the ability to change the events of a CSP process and the B machines when refining a system. Notions of refinement based on traces and on traces/divergences are introduced in which abstract, events arc, refined by sequences of concrete events. A complementary notion of refinement between B machines is also introduced, yielding compositionality results for refinement of CSP parallel to B controlled components. The paper also introduces a notion of I/O refinement into our action refinement framework.
Item Type: | Conference or Workshop Item (Conference Paper) | ||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Divisions : | Faculty of Engineering and Physical Sciences > Computer Science | ||||||||||||||||
Authors : | Schneider, S and Treharne, H | ||||||||||||||||
Date : | 2009 | ||||||||||||||||
DOI : | 10.1007/978-3-642-00255-7_8 | ||||||||||||||||
Contributors : |
|
||||||||||||||||
Depositing User : | Symplectic Elements | ||||||||||||||||
Date Deposited : | 29 Sep 2011 11:44 | ||||||||||||||||
Last Modified : | 06 Jul 2019 05:08 | ||||||||||||||||
URI: | http://epubs.surrey.ac.uk/id/eprint/7191 |
Actions (login required)
![]() |
View Item |
Downloads
Downloads per month over past year