Formal Modelling and Verification
in CSP
Course
contents:
CSP (Communicating and
Sequential Processes) is a formal language invented by Hoare, Brookes, and
Roscoe of Oxford in early 80s. It is designed specially to model and reason
concurrent and communicating systems, and has a comprehensive tool set to
support automatic verification based on a notion of refinement.
Many aspects of computer
systems involve some form of interaction between different identities. CSP has
been used extensively in the modelling and analysis
of hardware (e.g. synchronous/asynchronous circuits, processor RTL design,
etc.), software (objects,
components, UML, etc.) and distributed systems (distributed protocols, security
protocols, etc.).
In this course we will give
you a gentle introduction to CSP, concentrating on CSP operators, the concept
of deadlock, refusal and refinement, and the formal semantics (esp. operational
one). Examples are given to illustrate the ideas and some demonstration of
tools to sketch the procedure how to apply CSP on realistic problems. Finally
we will also mention some work on using CSP to formalise
UML and the benefits in doing so.
Synopsis:
1. Events and Processes: representing communication and
interaction; components and interfaces; levels of abstraction.
2. Interaction and deadlock:
internal and external choice; non-determinism; traces and refusals; process
refinement.
3. Concurrency: parallel
combination; specifying interfaces; static alphabets.
4. Abstraction: changing
levels of abstraction; mechanisms: interleaving, renaming, and hiding;
abstraction and non-determinism.
5. Applications: case studies
and applications, including: communication protocols; critical systems;
objects, classes, and threads.
References:
Tony Hoare (1985):
Communicating Sequential Processes, Prentice Hall.
http://www.usingcsp.com/cspbook.pdf
Bill Roscoe (1998): The
Theory and Practice of Concurrency, Prentice Hall.
http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.pdf
Steve Schneider (1999):
Concurrent and Real Time Systems: the CSP Approach, John Wiley.
Lecturer
Bio:
Dr. Xu Wang is currently a research fellow at the International
Institute for Software Technology, United Nations University. His research interests
lie in the broad field of semantic and verification of concurrent systems,
where he specialises in developing automatic
verification methods and state space reduction techniques for CSP/FDR. Before
joining UNU-IIST as an assistant research fellow in 2006, he worked as research
staff at HKUST, Oxford University and Birmingham University since 2000. He
holds PhD, M.Eng. and B.Sc.
degrees in Computer Science from Chinese Academy of Sciences and Xi'an Jiaotong University. He would like to work with motivated
students with interests in applying formal methods to solve practical problems
in concurrent systems.