This course wiki is under construction and reflects what was done last year. It will be updated at the start of the W20 term.

EECS3342 Winter 2019 Specification and Refinement

Video introducing Event-B/Rodin (Abrial).

Lab0 has been released for this week. Login and obtain Lab0 from the SVN tab in the sidebar.

• EECS3342 System Specification and Refinement Lecture Times:
  • Class TR 11.30am, LSB105
  • Scheduled Labs: Every Tuesday 1pm to 2pm in LAS1006. Lab attendance is required and there will be required labs, there is a Labtest almost every week.
  • In the Lab, we now use rodin3.4. See Resources. On an EECS/Linux workstation, type rodin (which is aliased to Rodin 3.4).

• Important: Subscribe to the forum for the latest announcements. Please ask all questions relating to the course material on the forum (not via email). For all other questions, see me during office hours.

• See bottom ↓ of this page for login with your Prism password. Slides are available from the SVN repository (see link in the sidebar, once you have logged on).

• Instructions for the Labs will be provided in the first lecture.

• Read the course outline regularly. It is important to read all the required readings (not all of which are discussed in class). It is important to do the suggested exercises.

• In the SVN → Readings, you will find the PDF for the Rodin 2.8 Manual. Please familiarize yourselves with all the material in the manual, during the first week of classes.

• Suggested Text: Jean-Raymond Abrial, Modeling in Event-B: System and Software Engineering, Cambridge 2010. Available in Steacie. See SVN for notes.

• See Event-B Information for notes on Equational Logic and also on the Sequent Calculus used by Event-B/Rodin. There is an online tutorial on the sequent calculus with point and click to try proofs. Rodin works somewhat differently but the underlying concepts are similar.

Theory and tools for specifying computer systems (sequential, concurrent and embedded). Specification (via set theory and predicate logic), modelling, abstraction, refinement and formal reasoning are undertaken before code development so that systems are correct by construction under the stated assumptions.

Prerequisites: General prerequisites (CSE2011 3.0 and a cumulative GPA of 4.5 or better over all completed major computer science courses and CSE1019 3.0), and MATH 1090

This course provides students with an understanding of how to use mathematics (set theory and predicate logic) to specify and design correct computer systems whether the systems are sequential, concurrent or embedded. The course stresses both the underlying theory as well as the ability to use industrial strength tools that can be applied in practice. User requirements are formalized via an abstract mathematical model that is amenable to formal reasoning long before any programming activity is undertaken (e.g. as done in Event-B, Z and VDM). Successive models are like blueprints in traditional engineering disciplines and their mathematical nature allows us to reason about and predict their safety properties.

After successful completion of the course, students are expected to be able to:

• Document requirements organizing them into appropriate categories such as environmental constraints versus functional properties (safety and progress).
• Construct high level, abstract mathematical models of a system (consisting of both the system and its environment) amenable to formal reasoning.
• Apply set theory and predicate logic to express functional and safety properties from the requirements as events, guards, system variants and invariants of a state-event model.
• Use models to reason about and predict their safety and progress properties.
• Plan and construct a sequence of refinements from abstract high-level specifications to implemented code.
• Prove that a concrete system refines an abstract model.
• Apply the method to a variety of systems such as sequential, concurrent and embedded systems.
• Use practical tools for constructing and reasoning about the models.
• Use Hoare Logic and Dijkstra weakest precondition calculus to derive correct designs

Chapters 1, 2, 3, 4, 5, 9 and 15 from the text Modeling in Event-B: System and Software Engineering, Jean-Raymond Abrial (Cambridge) makes this a possible textbook for the course.

This course is 3 hours of instruction per week as well as 1 hour of supervised labs per week.

The lab time is used to give students detailed exercises and instruction in using a practical verification tool (such as Rodin for Event-B) to accompany the material in the lectures. Tools are essential to using the theory and methods on larger examples and require expert knowledge of the use of automated theorem proving methods. Students will use such tools to prove the examples that are discussed in class as well as larger examples.

1. High-level state/event models and proof rules for invariant preservation

2. Refining a system and proving that the refinement preserves correctness

3. Proving convergence and absence of deadlock

4. Overview of system modelling constructs and proof rules for correctness in a reactive system

5. Design of a distributed systems illustrated with an ftp protocol

6. Anticipated events in high-level models for convergence

7. Use of contexts to develop relevant theories such as parity

8. Nondeterministic systems and associated safety invariant proof rules

9. Design of sequential programs with correction by construction via refinement rules

10. Hoare logic and weakest preconditions for program design and its use in a variety of developments

11. Methods for systematic development of correct-by-construction of reactive systems, illustrated with a train system

12. Thinking before Programming using Lamport’s TLA+ specification method

A good model may be used to predict its safety and fitness for purpose – before we start implementing the design. Thus we wish to show that our medical devices, aeroplanes, autonomous cars, power plants etc. are safe and reliable.