Course Material
19/9/12
Topic: Introduction
Lecture: slides (small)
Exercise: Sheet 1
Solution: Sheet 1
26/9/12
Topic: A Refresher on First-Order Logic and Set Theory
Lecture: slides, 4-up handout
Exercise: Sheet 2, prp.zip,prd.zip,profiles
Solution: prp-sol.zip, prd-sol.zip
3/10/12
Topic: A Refresher on First-Order Logic and Set Theory (cont.)
Lecture: Sheet 3, set.zip
Exercise: Sheet 3,
Solution: set-sol.zip, 03-family-sol.zip
Topic: Event-B by Examples: Controlling Cars on a Bridge
Lecture: slides, 4-up handout, text (Chapter 2), ch2_car.zip
10/10/12
Topic: Event-B by Examples: Controlling Cars on a Bridge (cont.)
Lecture: --
Exercise: Sheet 4, 04-numbers.zip, 04-proofs.zip
Solution: Sheet 4, 04-solution.zip
17/10/12
Topic: Types and Well-definedness
Lecture: slides, 4-up handout
Exercise: Sheet 5, 05-crazy-birthday.zip
Solution: Sheet 5
24/10/12
Topic: Event-B by Examples: Leader Election on a Ring-shaped Network
Lecture: slides, 4-up handout, LeaderElectionLHR-121010-Rodin-2.6.0.zip
Exercise: Sheet 6, 06-assignments.zip
Solution: Sheet 6, 06-solutions.zip
31/10/12
Topic: Event-B by Examples: Leader Election on a Ring-shaped Network (cont.)
Lecture: --
Exercise: Sheet 7, 07-assignments.zip
Solution: Sheet 7, 07-solutions.zip
7/11/12
Topic: Event-B Summary: Modelling Notation
Lecture: slides, 4-up handout
Topic: Event-B Summary: Proof Obligations
Lecture: slides, 4-up handout
14/11/12
Topic: Introduction to Model Checking
Lecture: slides, small
Exercise: Sheet 8
Solution: Sheet 8
Topic: Transition Systems and Linear-time Temporal Logic
Lecture: slides, small
Exercise: Introduction to PROMELA
21/11/12
Topic: Automata-theoretic Approach to Model Checking
Lecture: slides, small
Exercise: Sheet 9
Solution: Sheet 9
28/11/12
Topic: State-space exploration in SPIN
Lecture: slides, small
Exercise: Sheet 10
Solution: Sheet 10
5/12/12
Topic: Bounded Model Checking
Lecture: slides, small
Exercise: Sheet 11
Solution: Sheet 11
12/12/12
Topic: Bounded Model Checking (cont.)
Lecture: --
Exercise: Sheet 12
Solution: Sheet 12
19/12/12
Topic: Counterexample Guided Abstraction Refinement
Lecture: slides, small
Background Material
- Jean-Raymond Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press. ISBN 978-0-521-89556-9
- Matthias Schmalz. The Logic of Event-B. (in particular, p. 50-59)
- Ken Robinson. A Concise Summary of the Event-B Mathematical Toolkit.
- Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008. ISBN 978-0-262-02649-9
- Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004 (2nd edition). ISBN 978-0521543101
Rodin
We provide the Rodin platform for the following operating systems. Note that you need a java runtime environment (JRE, version 6 or newer) to run the tool. The 64-bit versions of Rodin will only run if a 64-bit version of Java is installed.
- Rodin for Windows 32-bit
- Rodin for Windows 64-bit
- Rodin for Linux 32-bit
- Rodin for Linux 64-bit
- Rodin for Mac OS X
Event-B wiki: wiki.event-b.org
Rodin handbook: handbook.event-b.org
SPIN
- Main page: www.spinroot.com
- Installing SPIN: readme file (with links)
- Documentation: PROMELA and SPIN's command-line options and more
- A forum for SPIN users
Recommended readings:
- Model checking: algorithmic verification and debugging by Clarke, Emerson, and Sifakis (Communications of the ACM, 2009)
- A Decade of Software Model Checking with SLAM by Ball, Levin, and Rajamani (Communications of the ACM, 2011)