T3 An Introduction to CSP || B
|
Tutors: |
Helen Treharne
Steve Schneider |
Affiliation: |
University of Surrey, UK |
Tutor: |
Neil Evans |
Affiliation: |
AWE, UK |
|
Date: |
August 21, 2006 |
Time:
|
2:00-5:30, 1/2hr break at 3:30 |
Location: |
ITB 222 |
Format: |
Half-day (afternoon), split into smaller sessions. Slides for the tutorial are available
for download from http://www.csp-b.org, and will also
be made available in printed form. |
| |
Topic:
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.
|
Objective:
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.
|
Prerequisites:
Tutorial assumes no prior knowledge of CSP||B.
Background papers can be found at http://www.csp-b.org
|
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.
|
