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.

There is an academic integrity website with comprehensive information about academic honesty and how to find resources at York to help improve students' research and writing skills, and cope with University life. Students are expected to review the materials on the SPARK Academic Integrity module.

York University is committed to principles of respect, inclusion and equality of all persons with disabilities across campus. The University provides services for students with disabilities (including physical, medical, learning and psychiatric disabilities) needing accommodation related to teaching and evaluation methods/materials. These services are made available to students in all Faculties and programs at York University.

Students in need of these services are asked to register with disability services as early as possible to ensure that appropriate academic accommodation can be provided with advance notice. You are encouraged to schedule a time early in the term to meet with each professor to discuss your accommodation needs. Please note that registering with disabilities services and discussing your needs with your professors is necessary to avoid any impediment to receiving the necessary academic accommodations to meet your needs.

Additional information is available at the following websites:

• Counselling & Disability Services
• York Accessibility Hub