System Specification and Refinement

Winter 2014

York University

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.

- Apr 19: Here is an Event-B model for the insertion sort problem; the pseudocode for the resulting algorithms is here.
- Apr 18: You may bring one page (two-sided) of handwritten notes to the exam. You will be given a copy of the Concise Summary of the Event B mathematical toolkit and a list of inference rules that should be sufficient for the exam.
- Apr 16: The office hour on April 17 is cancelled; instead, an office hour will be held on April 19 at 2pm in LAS 1002.
- Apr 16: Another solution to the defensive celebrity problem that includes a proof of deadlock freedom can be found here.
- Apr 14: Today's office hours is rescheduled to tomorrow April 15 at 3pm.
- Apr 4: The office hours will be held at the normal times until the final exam on April 21 unless otherwise indicated here.
- Apr 4: A solution to the defensive celebrity problem discussed in the labs can be found here.
- Mar 25: The solutions to assignment 1 are here.
- Mar 21: The deadline for Assignment 2
**is extended to March 22 at 09:00**. This is the last extension. - Mar 20: The project is out. You can find Abrial's description of the electronic hotel key system problem here. The preliminary requirements document is due on March 26 at 17:00 and the omplete final report is due on April 4 at 23:59.
- Mar 17 & 18: The deadline for Assignment 2
**is extended to March 21 at 17:00**. - Mar 12: Due to the weather emergency declaration, today's office hour at 15:00 is cancelled.
- Mar 12: Here, you can find the selection sort model that Simon discussed in the lab yesterday (as a Rodin archive). The textbook's version can be found here.
- Mar 6: Assignment 2 is out; it is due
**March 21 at 17:00 (extended!)**. - Feb 26: The deadline for Assignment 1
**is extended to March 1 at 17:00**. - Feb 26: The office hour today is cancelled. Please come to tomorrow's office hour instead.
- Feb 25: The lab exercise this week is to develop an Event-B model
that solves the
*celebrity problem*. You can find a partially completed model in this Celebrity.zip archive. Import it into Rodin and follow the instructions in Section 2.9 of the Rodin Handbook. - Feb 23: The office hour on Feb 24 at 15:00 is rescheduled to Feb 25 at 15:00 in LAS 3052.
- Feb 19: The office hour on Feb 19 is cancelled. Elnaz will do an office hour on Feb 20 at 2pm in LAS 3052.
- Feb 19: The solution to the NOR question in the labtest is here; the proofs are done as shown in the NAND lab document. The solution to the traffic lights question in the labtest is here; the proofs obligations can be discharged with minimal intervention.
- Feb 14: Assignment 1 is out; it is due
**March 1 at 17:00 (extended!)**. - Feb 5: The solutions to the traffic lights lab are available here.
- Feb 4: Here are the files for the Feb 4 lab: 3342-Lab2.pdf , nand-gate-spec.pdf , PredicateLogic.pdf , PredicateLogic-Simple.zip , PredicateLogic-Complex.zip .
- Feb 4: Here is a Event B Reference Card and a Concise Summary of the Event B mathematical toolkit (both by Ken Robinson).
- Jan 30:
**Labtest 1 will be on Feb. 11 during the lab.** - Jan 29: You should read the Rodin Handbook to get more information on how to use the tool.
- Jan 28: At the lab on Jan 28, Simon will discuss a system involving building a table of cubes without using multiplications. This zip file cubes.zip contains the project.
- Jan 23: We have created a forum for the course where students can post questions about course material and all students can see our answers. Questions about using the Rodin tool and the lab exercises are especially encouraged. But any topic of the course can be discussed.
- Jan 20: At the lab on Jan 21, Simon will discuss a system involving traffic lights. This zip file trafficlights.zip contains the project. Simon will explain how to import it into the Rodin platform.
- Classes start January 7.

Prof. Yves Lespérance

Office: LAS 3052A

Tel: 736-2100 ext. 70146

Email: `lesperan "at" cse.yorku.ca`

Tuesday and Thursday 11:30 to 13:00 in SC 205.

Tuesday 13:00 to 14:00 in LAS 1002A.

Monday and Wednesday from 15:00 to 16:00, and Thursday from 14:00 to 15:00 in LAS 3052A.

Jean-Raymond Abrial.
*Modeling in Event-B: System and Software Engineering*.
Cambridge University Press, 2010.

The Event-B web site and the Event-B and Rodin Documentation Wiki.
The **Rodin** platform is available on the Event-B web site and
installed in the Prism lab.

The textbook is recommended but not required; it is available at the York University Bookstore. Lecture notes are available on the Event-B web site that cover much of the material in the book.

General prerequisites and SC/MATH 1090 3.00.

Labtest | 5% |

Assignement 1 | 10% |

Assignement 2 | 15% |

Project | 20% |

Final exam | 50% |

Total | 100% |

For the project, you can work on your own or work with one partner (a team thus has at most 2 members).

It is important that you look at the departmental guidelines on academic honesty. Although you may discuss the general approach to solving a problem with other people, you should not discuss the solution in detail. You must not take any written notes away from such a discussion. Also, you must list on the cover page of your solutions any people with whom you have discussed the problems. The solutions you hand in should be your own work. While writing them, you may look at the course textbook and your own lecture notes but no other outside sources.

- Week 1 (Jan 6) Introduction

*Recommended Readings:*Abrial textbook Chapter 1.

Slides on Chapter 1. - Weeks 2 & 3 (Jan 13 & 20) Systems: Controlling Cars on a Bridge

*Recommended Readings:*Abrial textbook Chapter 2.

Slides on Chapter 2. - Week 4 (Jan 27) A Mechanical Press Controller

*Recommended Readings:*Abrial textbook Chapter 3.

Slides on Chapter 3. - Week 5 (Feb 3) A Simple File Transfer Protocol

*Recommended Readings:*Abrial textbook Chapter 4.

Slides on Chapter 4. - Week 6 (Feb 10) The Event-B Modeling Notation

*Recommended Readings:*Abrial textbook Chapter 5 Section 1. This material is also discussed in Section 3.2 of the Rodin Handbook. - Weeks 7 & 8 (Feb 24 & Mar 3) Development of Sequential Programs

*Recommended Readings:*Abrial textbook Chapter 15.

Slides on Chapter 15. - Week 9 (Mar 10) Event-B Proof Obligation Rules

*Recommended Readings:*Abrial textbook Chapter 5 Section 2. This material is also discussed in Section 3. 2 of the Rodin Handbook. - Week 10 & 11 (Mar 17 & 24) The Event-B Mathematical Language

*Recommended Readings:*Abrial textbook Chapter 9. (See also the Event-B Mathematical Language page on the Event-B Wiki for a discussion of differences between the version of the mathematical language in the textbook and slides and the one used in the Rodin tool.)

Slides on Chapter 9. - Week 12 (Mar 31) Concurrent Program Development

*Recommended Readings:*Abrial textbook Chapter 7.

Slides on Chapter 7.

George Tourlakis.
*Mathematical Logic*.
Wiley, 2008.