University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Communicating B Machines.

Schneider, S and Treharne, H (2002) Communicating B Machines. Lecture Notes in Computer Science, 2272. pp. 416-435.

fulltext.pdf - Accepted version Manuscript
Available under License : See the attached licence file.

Download (269kB)
[img] Text (licence)

Download (1kB)


This paper describes a way of using the process algebra CSP to enable controlled interaction between B machines. This approach supports compositional verification: each of the controlled machines, and the combination of controller processes, can be analysed and verified separately in such a way as to guarantee correctness of the combined communicating system. Reasoning about controlled machines separately is possible due to the introduction of guards and assertions into description of the controller processes in order to capture assumptions about other controlled machines and provide guarantees to the rest of the system. The verification process can be completely supported by difierent tools. The use of separate controller processes facilitates the iterative development and analysis of complex control flows within the system. The approach is motivated and illustrated with a non-trivial running example.

Item Type: Article
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
Schneider, S
Treharne, H
Date : 2002
DOI : 10.1007/3-540-45648-1_22
Contributors :
ContributionNameEmailORCID, D, JP, MC, K,
Related URLs :
Depositing User : Mr Adam Field
Date Deposited : 29 Sep 2011 13:13
Last Modified : 31 Oct 2017 14:09

Actions (login required)

View Item View Item


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