CSE 3342
System Specification and Refinement
Winter 2014
Department of Electrical
Engineering & Computer Science,
York University
Course Description
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.
What's New
- 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.
Instructor
Prof. Yves Lespérance
Office: LAS 3052A
Tel: 736-2100 ext. 70146
Email: lesperan "at" cse.yorku.ca
Lectures
Tuesday and Thursday 11:30 to 13:00 in SC 205.
Mandatory Lab
Tuesday 13:00 to 14:00 in LAS 1002A.
Instructor Office Hours
Monday and Wednesday from 15:00 to 16:00, and Thursday from 14:00 to 15:00 in LAS 3052A.
Textbook
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.
Prerequisites
General prerequisites and SC/MATH 1090 3.00.
Evaluation Scheme
| 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).
Academic Honesty
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.
Readings and Lecture Transparencies
Additional References
George Tourlakis.
Mathematical Logic.
Wiley, 2008.