Time: Monday and Wednesday, 9:00-10:30
Location: Victor Phillip Dahdaleh Building, room 0009
Instructor: Franck van Breugel, franck@eecs.yorku.ca
Office Hours: Monday and Wednesday, 10:30-11:30 or by appointment, Lassonde Building, room 3046
Teaching assistant: Amgad Rady

Time: Friday, 10:00-11:00
Location: Lassonde Building, lab 1004

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.

Also the notes

• Franck van Breugel. Java PathFinder: a tool to detect bugs in Java code. 2020.

will be used. Additional reading material will be provided on this course wiki.

Students are evaluated based on

• three quizzes (10% each)
• a midterm (10%)
• a final exam (10%)
• a project (50%)
  • installing JPF (5%)
  • draft project proposal (2%)
  • project proposal (3%)
  • first progress report (5%)
  • second progress report (5%)
  • presentation (10%)
  • report (10%)
  • code (10%)

Students can view their marks using the ePost system.

Very brief descriptions of the last four years' projects can be found here. A sample of a draft proposal can be found here.

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.

We recognize that many Indigenous nations have longstanding relationships with the territories upon which York University campuses are located that precede the establishment of York University. York University acknowledges its presence on the traditional territory of many Indigenous Nations. The area known as Tkaronto has been care taken by the Anishinabek Nation, the Haudenosaunee Confederacy, the Wendat, and the Métis. It is now home to many Indigenous Peoples. We acknowledge the current treaty holders and the Mississaugas of the Credit First Nation. This territory is subject of the Dish With One Spoon Wampum Belt Covenant, an agreement to peaceably share and care for the Great Lakes region.

Information about York's Indigenous Framework can be found online.

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 in 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:

• Student Accessibility Services
• York Accessibility Hub
• York's Senate Policy on Academic Accommodation for Students with Disabilities

York students are subject to the York University Policy for the Ethics Review Process for Research Involving Human Participants. In particular, students proposing to undertake research involving human participants (e.g., interviewing the director of a company or government agency, having students complete a questionnaire, etc.) are required to submit an Application for Ethical Approval of Research Involving Human Participants at least one month before you plan to begin the research. If you are in doubt as to whether this requirement applies to you, contact your Course Director immediately.

York University is committed to respecting the religious beliefs and practices of all members of the community, and making accommodations for observances of special significance to adherents. Should any of the dates specified in this syllabus for an in-class test or examination pose such a conflict for you, contact the course director within the first three weeks of class. Similarly, should an assignment to be completed in a lab, practicum placement, workshop, etc., scheduled later in the term pose such a conflict, contact the course director immediately. Please note that to arrange an alternative date or time for an examination scheduled in the formal examination periods (December and April/May), students must complete an Examination Accommodation Form, which can be obtained from Student Client Services, Student Services Centre or online. More information can be found online.

Students and instructors are expected to maintain a professional relationship characterized by courtesy and mutual respect. Moreover, it is the responsibility of the instructor to maintain an appropriate academic atmosphere in the classroom and other academic settings, and the responsibility of the student to cooperate in that endeavour. Further, the instructor is the best person to decide, in the first instance, whether such an atmosphere is present in the class. The policy and procedures governing disruptive and/or harassing behaviour by students in academic situations is available online.