FM 2006

August 21 - 27, 2006
McMaster University
Hamilton ON, Canada

Submission Dates

Technical Papers, Workshops and Tutorials

Friday February 24, 2006

Posters and Tools, Doctoral Symposium

Friday May 26, 2006


Notification Dates

Technical Papers

Friday April 28, 2006

Workshops and Tutorials

Friday March 10, 2006

Doctoral Symposium

Wednesday June 14, 2006

Posters and Research Tools

Monday June 12, 2006

Contact Information

General Inquiries

General Chair

Emil Sekerinski

Program Chairs

Jayadev Misra,
Tobias Nipkow

Workshops Chair

Tom Maibaum

Tutorials Chair

Jin Song Dong

Tools & Poster Chair

Marsha Chechik

Industry Day Chairs

Volkmar Lotz,
Asuman Suenbuel

Doctoral Symposium Chair

Ana Cavalcanti

Augusto Sampaio

Jim Woodcock

Sponsorship Chair

Jürgen Dingel

T3 An Introduction to CSP || B
Helen Treharne
Steve Schneider
University of Surrey, UK
Neil Evans
August 21, 2006
2:00-5:30, 1/2hr break at 3:30
ITB 222
Half-day (afternoon), split into smaller sessions. Slides for the tutorial are available for download from, and will also be made available in printed form.


Large scale programming often adopts a strong separation between the model, view and controller aspects of a system. One benefit of this widely used technique is the isolation of the state of the model from its co-ordinating software. This enables a programmer to focus on different parts of a system individually. We believe that a similar separation of concerns is also appropriate at the specification level. State-based methods are primarily concerned with describing the state of a system together with its associated properties whereas event-based methods support the formal description of components which interact in a co-ordinated way.

The tutorial will introduce the CSP||B approach which combines a state and an event based method to support the specification of complex interacting systems.

The tutorial is structured as follows:

An overview of the B-Method and the process algebra CSP, and their respective tool support. A discussion of how they can be combined will be illustrated and the theoretical aspects of the combination will be explained.

The method supports verifying complex properties of a system expressed in CSP and B. These properties are commonplace in distributed systems. The tutorial will discuss the verification process by working through two case studies: a distributed protocol and a model of a biological system. The protocol illustrates the applicability of CSP||B to analysing communication systems, and our abstract model of haemostasis illustrates how CSP||B can be used in an interdisciplinary way.


By the end of the session participants will have an appreciation of how to develop specifications using CSP||B and how to conduct formal analysis of the specifications.


Tutorial assumes no prior knowledge of CSP||B.
Background papers can be found at

Biography of Tutor:

Dr Helen Treharne will co-ordinate the tutorial. She is a lecturer at the University of Surrey. She is part of a group behind the development of the theoretical foundations for CSP||B. She has previous industrial experience of using the B-Method to develop embedded software.

Professor Steve Schneider is Head of Computing at the University of Surrey. He has been working in the area of formal methods and security for over 10 years. He has published several books including ones on the B-Method and on the CSP approach to real-time and concurrent systems. He has made a significant contribution to research in process algebra, its timed extensions, and its application.

Dr Neil Evans is a Senior Formal Methods Developer at AWE, UK. He was previously involved in the RODIN project investigating open source tool support for verification of B developments. He has extensive experience of using the theorem prover PVS to the verifying security properties and contributed to the foundations of CSP||B.