University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Verifying controlled components

Schneider, Steve A. and Treharne, Helen (2004) Verifying controlled components

[img]
Preview
PDF
fulltext.pdf

Download (258Kb)

Abstract

Recent work on combining CSP and B has provided ways of describing systems comprised of components described in both B (to express requirements on state) and CSP (to express interactive and controller behaviour). This approach is driven by the desire to exploit existing tool support for both CSP and B, and by the need for compositional proof techniques. This paper is concerned with the theory underpinning the approach, and proves a number of results for the development and verification of systems described using a combination of CSP and B. In particular, new results are obtained for the use of the hiding operator, which is essential for abstraction. The paper provides theorems which enable results obtained (possibly with tools) on the CSP part of the description to be lifted to the combination. Also, a better understanding of the interaction between CSP controllers and B machines in terms of non-discriminating and open behaviour on channels is introduced, and applied to the deadlock-freedom theorem. The results are illustrated with a toy lift controller running example.

Item Type: Conference or Workshop Item (UNSPECIFIED)
Additional Information: This is a pre-press version of an article published in Lecture Notes in Computer Science, 2999, 87-107. Click here to access the published version. © 2004 Springer. Presented at IFM'04: Integrating Formal Methods. Winner of the best paper award.
Divisions: Faculty of Engineering and Physical Sciences > Computing Science
Depositing User: Mr Adam Field
Date Deposited: 27 May 2010 14:45
Last Modified: 23 Sep 2013 18:35
URI: http://epubs.surrey.ac.uk/id/eprint/1890

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