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)
JavaScript has been disabled in your browser