The SVN will have a list of exercises (currently Ex1, Ex2 and 9 questions in Ex3) that you must do on your own to test your knowledge of the material and to help you to prepare for the labtests and exam.

Background Readings

• What/Why formal methods? Slides Chap. 1: Introduction.
• Textbook Chapter I (pages 1-16).

Tuesday: 01 slides MathsAndEngineering.pptx (why testing is not enough) and 02 slides BuildingSoftwareReliability.pptx (developing good software development skills such as contracts/assertions and good coding/testing methods).

Thursday: 03-Requirements slides. The notion of atomic requirements. The difference between R-statements (in the optative mood) and E-statements about the environment (in the indicative mood). Event-B mathematical models: contexts and machines. A simple bank as an example.

Required: You must do the first Exercise (Ex1-prop) in the SVN. This involves familarizing yourself with the Rodin tool, and using Rodin to do propositional logic in contexts.

Covered Rodin bank account in the 03-Requirements slides. Atomic requirements. Contexts verus machines in Event-B. The Rodin tool. Functions and function updates. Invariant perservation.

Complete the bank account example: using function update; modelling REQ 3 for credit limits as an invariant; introduce the set of accounts managed by the bank and associated invariant.

• Read the Rodin Users handbook up to and including Section 2.5.2 (its on the SVN and there are links to it from Resources).

• Bridge controller (reactive systems)
  • The initial Event-B model for the bridge controller (up to slide 33 of Chapter 2: Controlling cars on a bridge).
  • Required readings: Read up to end of the second refinement of chapter 2 from the sample textbook.

Topics covered by the bridge controller include

• Initial models and Proof rules for invariant preservation
• Refinement/correct by construction
• Proof rules for refinement
• Deadlock prevention and relative deadlock
• Divergence, Convergent events and variants
• Proof rules including SIM
• Controller events and Environment events

Chapter 4 of the optional textbook – A simple File Transfer Protocol (FTP).

• ftp slides

In the previous example, the program was reactive (i.e. it had to control an external situation such as cars on a bridge). This chapter deals with a protocol used on a computer network to transfer data from a sender to a receiver. The example will also allow us to extend our mathematical language with sets, functions and relations. As usual we will start with a requirements document. The initial model tells us what the protocol is supposed to achieve without telling us how to achieve it; how to achieve it will be dealt with in succesive refinements. Note that the model presented in the slides (using the notion of an anticipated event) is different than that of the textbook.

In the second refinement in the ftp protocol we did separate the sending and receiving agent. We had a lab session with Rodin, proving cross-products, powersets, relations and functions.

Third and final refinement in which we add a parity bit. The distributed ftp protocol is now ready to be implemented in code (how would you write the program?) with a guarantee that it will terminate with the file properly transmitted from the sender to the receiver. Lab: prove the parity bit theorem.

Try a manual proof of the theorem needed for the theory of parity (in the ftp protocol). This theorem might be hard to prove. The suggestion is to first do the proof manually, which then makes it easier to do in Rodin. Using this approach, we were able to derive a Lemma that was helpful in the Rodin proof.

Exercises 11 and 12 in preparation for Labtest2: Ex 11: ftp protocol. Ex12: Do the initial model of the celebrity example (from the Exercises). Formalize the problem in Event-B using a “knows” relation. Recall the indentity and inverse relations and show how the Celebrity axioms could be written in predicate logic or set theory. The celebrity example is one of the exercises that you must do in advance of Labtest2.

Required reading: all of chapter IV and chapter V (Event-B proof obligation rules). Injections, surjections and bijections in Event-B. Review: Relations, functions, identity relation, inverse. Feasibility proof obligations for non-deterministic assignment, witness (WITH) for local variable refinements, convergence and proof obligations.

Requirements for the sorting algorithm. Initial specification using an anticipated event. First and second refinements leading to the use of merge rules for a loop within a loop. For the slides see Sequential Programs.

Discussion. (a) Data refinement and Procedural Refinement. Illustration of these concepts using the Birthday Book example in which we write an initial specification, do a data refinement, followed by a procedural refinement; finally a merge produces code. (b) BAG abstract datatype.

In class we provided the following requirement:

REQ: Find an integer approximation to the square root of n.

Specification

n,d: INT

sqrt

require n >= 0
ensure (d^2 <= n < (d+1)^2) & (n = old n) 

Problem: Convert the following specification ito Rodin and use Rodin refinement rules to develop the code for the method sqrt.

Tuesday: Dijkstra weakest precondition calculus and loop variants and invariants.Proving loop termination. Relationship of Dijkstra weakest precondition calculus to Event-B. Slides on the SVN.

Thursday: Review of arithmetic, set theory, predicate logic and Event-B invariant and refinement proof obligations. Translation between set theoretic statements and predicate logic. Re-write rules.