Time: Mondays, 10:30-12:00 and Tuesdays, 14:30-16:00
Location: Stong College, room 221 (Mondays) and TEL Building, room 0004 (Tuesdays)
Instructor: Franck van Breugel, franck@cse.yorku.ca
Office Hours: to be determined, Lassonde Building, room 3046

Time: Thursdays, 14:30-15:30
Location: Lassonde Building, lab 1004
Teaching Assistant: Qiyi Tang, qiyitang@cse.yorku.ca

This course is a sequel to System Specification (EECS3342) which is an introduction to mathematical modeling and refinement of systems using deductive methods.

This course provides students with a deeper understanding of both deductive and algorithmic methods and tools for ensuring the safety and correctness of mission critical systems (e.g. medical devices such as pacemakers, nuclear reactors and train control systems). In addition to deductive techniques, the course treats algorithmic methods such as model-checking tools, specification languages such as temporal logic, table based specification methods, and the nature of software certification.

• The ability to explain the importance of safety-, mission-, business-, and security-critical systems.
• Demonstrated knowledge of the importance of good software engineering practices for critical systems.
• The ability to use rigorous software engineering methods to develop dependable software applications that are accompanied by certification evidence for their safety and correctness.
• Knowledge of the method and tools using deductive approaches (such as theorem proving).
• Knowledge of methods and tools for algorithmic approaches (such as model checking, bounded satisfiability) etc.
• Knowledge of the theory underlying deductive and algorithmic approaches.
• The ability to use industrial strength tools associated with the methods on large systems.

The textbook for this course is

• Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press. 2008.

Additional reading material will be provided on this course wiki.

Students are evaluated based on

• weekly quizzes (5% each)
• a project (20%)
• a final exam (20%)

Students can view their marks using the ePost system.

During quizzes and the final exam, students are expected to do their own work. Looking at someone else's work during the test, talking during the test, using aids not permitted (such as a phone) during the test, and impersonation are all examples of academically dishonest behaviour. Students are expected to read the Senate Policy on Academic Honesty.