Supplementary Information for COMP60110

This course is largely based on the superb material for teaching Event-B
prepared by Jean-Raymond Abrial, and associated with the Event-B book
(J-R. Abrial, Event-B, Cambridge University Press, to appear).
A huge thank you to Jean-Raymond for permission to use this stuff.

Course Plan and Downloads

Week 1

Introduction to Formal Methods in System Design.
Introduction to the Event-B Methodology.

Case study: Cars on a Bridge.
Cars Rodin Archive (.zip)

Practical Work: Getting Started with Rodin and Exercises 1.

Week 2

Review of Exercises 1.

Case study: Developing a File Transfer Protocol.
File Transfer Rodin Archive (.zip)
Bounded Retransmission Rodin Archive (.zip)

Mechanical Proof.

Practical Work: Exercise 2, complete development of
a variant of the file transfer protocol.

Week 3

Case studies: Leader Election, Synchronising Processes.

Developing Sequential Programs.

Project Allocation.

Practical Work: Exercise 3, complete development of
a toy postal system.

Week 4

Case study: A Mechanical Press Controller.

Practical Work: Project Work

Week 5

Project Work
Overall Course Assessment.
Exam: 50%, Project: 40%, Exercises 2 and 3: 10%

Course Slides

Course Slides (.pdf)

General Resources

Getting Started with Rodin (.pdf)        Rodin User Manual (.pdf)        CS60110 Exercises (.pdf)

Simple Latex Documents (.pdf)        b2latex.sty (.sty)

Latex Template (.pdf)        Latex Template (.tex)        Rodin Screenshot (.png)        LaTeX Mathematical Symbols (.html)