CSP-B - A New Composition of Process Algebra and State-based Specification

Steve Schneider

(Royal Holloway)

This talk describes a way of using the process algebra CSP to control B machines and to enable interaction between them. 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 the 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 different tools. The use of separate controller processes facilitates the iterative development and analysis of complex control flows within the system.
Tuesday 11th March 2003, 14:00
Robert Recorde Room
Department of Computer Science