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


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.

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.


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.

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.