University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Chunks: Component verification in CSP||B

Schneider, S, Treharne, H and Evans, N (2005) Chunks: Component verification in CSP||B In: 5th International Conference on Integrated Formal Methods, 2005-11-29 - 2005-12-02, Eindhoven, Netherlands.

[img]
Preview
Text
chunks.pdf - Accepted version Manuscript
Available under License : See the attached licence file.

Download (194kB)
[img] Text (licence)
licence.txt

Download (1kB)

Abstract

CSP||B is an approach to combining the process algebra CSP with the formal development method B, enabling the formal description of systems involving both event-oriented and state-oriented aspects of behaviour. The approach provides architectures which enable the application of CSP verification tools and B verification tools to the appropriate parts of the overall description. Previous work has considered how large descriptions can be verified using coarse grained component parts. This paper presents a generalisation of that work so that CSP vertical bar vertical bar B descriptions can be decomposed into finer grained components, chunks, which focus on demonstrating the absence of particular divergent behaviour separately. The theory underpinning chunks is applicable not only to CSP vertical bar vertical bar B specification but to CSP specifications. This makes it an attractive technique to decomposing large systems for analysing with FDR.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
NameEmailORCID
Schneider, SUNSPECIFIEDUNSPECIFIED
Treharne, HUNSPECIFIEDUNSPECIFIED
Evans, NUNSPECIFIEDUNSPECIFIED
Date : 2005
Identification Number : 10.1007/11589976_7
Contributors :
ContributionNameEmailORCID
http://www.loc.gov/loc.terms/relators/EDTRomijn, JUNSPECIFIEDUNSPECIFIED
http://www.loc.gov/loc.terms/relators/EDTSmith, GUNSPECIFIEDUNSPECIFIED
http://www.loc.gov/loc.terms/relators/EDTVanDePol, JUNSPECIFIEDUNSPECIFIED
http://www.loc.gov/loc.terms/relators/PBLSpringer, UNSPECIFIEDUNSPECIFIED
Uncontrolled Keywords : component based verification, B-method, CSP, decomposition
Depositing User : Symplectic Elements
Date Deposited : 29 Sep 2011 13:08
Last Modified : 31 Oct 2017 14:09
URI: http://epubs.surrey.ac.uk/id/eprint/7192

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