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.
Case study: Cars on a Bridge.
Cars Rodin Archive (.zip)
Practical Work: Getting Started with Rodin and 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.
Developing Sequential Programs.
Project Allocation.
Practical Work: Exercise 3, complete development of
a toy postal system.
Practical Work: Project Work
Simple Latex Documents (.pdf) b2latex.sty (.sty)
Latex Template (.pdf) Latex Template (.tex) Rodin Screenshot (.png) LaTeX Mathematical Symbols (.html)