CS 4830/7485: System Specification, Verification, and Synthesis, Fall 2019

Khoury College of Computer Sciences
Northeastern University

Instructor: Prof. Stavros Tripakis (also spelled Trypakis)

Class: Mon and Wed, 2:50-4:30PM, Hastings Suite 202

Office hours: WVH 340, Mon and Wed 4:30-5:30PM, or by request

Introduction

What predictions can we make about the software that we write? Can we predict that our program will never crash? That its output will be correct? What does "correct" mean, exactly? And what predictions can we make about safety-critical, embedded, cyber-physical, and all sorts of other systems that heavily rely on software? This course covers the fundamentals in formal system modeling, specification, verification, and synthesis, with a focus on automated methods (model checking, computer-aided verification and synthesis).

Goals:

  1. Understand the fundamental concepts in modern system theory.
  2. Learn how to formally model systems and specify their correctness.
  3. Learn the basic algorithmic techniques for checking that a system satisfies its specification (model-checking).
  4. Learn the basic techniques for automated system synthesis.
  5. Be able to use model-checkers such as Spin and NuXMV.

Schedule

The schedule below will be updated as we go along:

Lecture #, Date
Topics, slides, code, other material
Suggested readings
Class 01,
4 Sep 2019		 1. Introduction; The science of software and systems; Logistics; Slides: 01-intro.pdf Chapter 1 of Baier-Katoen; CACM paper How Amazon Web Services Uses Formal Methods
Class 02,
9 Sep 2019		 2. Systems; System design methods; Slides: 02-systems.pdf
3. Finite state machines; Modeling FSMs in nuXmv; Slides: 03-state-machines.pdf 		RAND report Driving to Safety; Lamport paper Computation and State Machines
Class 03,
11 Sep 2019		 4. Transition systems; Promela and Spin; Slides: 04-transition-systems.pdf Chapter 2 of Baier-Katoen
Class 04,
16 Sep 2019		 5. System composition; Synchronous composition; Slides: 05-synchronous.pdf Chapter 2 of Baier-Katoen; Malik paper Analysis of Cyclic Combinational Circuits
Class 05,
18 Sep 2019		 6. Asynchronous composition; Slides: 06-asynchronous.pdf;
7. The state-space explosion problem; Slides: 07-state-explosion.pdf 		Chapter 2 of Baier-Katoen; Alur-Tripakis paper Automatic Synthesis of Distributed Protocols
Class 06,
23 Sep 2019		 8. Fairness; Slides: 08-fairness.pdf Chapter 3 of Baier-Katoen; Piterman-Pnueli paper Temporal Logic and Fair Discrete Systems;
Class 07,
25 Sep 2019		 9. Specification; Temporal logic; LTL; Slides: 09-spec-ltl.pdf Chapter 5 of Baier-Katoen (up to 5.2); A primer on logic (draft)
Class 08,
30 Sep 2019		 9. LTL continued: The LTL model-checking problem; Invariants in LTL; LTL in Spin; Slides: 09-spec-ltl.pdf
10. Safety and liveness; Slides: 10-safety-liveness.pdf 		Alpern-Schneider paper Defining Liveness;
Class 09,
2 Oct 2019		 11. CTL; Slides: 11-ctl.pdf Chapter 6 of Baier-Katoen (up to 6.4);
Class 10,
7 Oct 2019		 Homework 2 solution review;
Class 11,
9 Oct 2019		 12. Reachability analysis; Slides: 12-reachability.pdf Baier-Katoen, Section 3.3.1 and Appendix A.4
Class 12,
16 Oct 2019		 Exam 1
Class 13,
21 Oct 2019		 13. Symbolic methods; Symbolic representation of state spaces; Symbolic reachability; Slides: 13-symbolic.pdf Baier-Katoen, Sections 6.7.1 and 6.7.2
Class 14,
23 Oct 2019		 14. Binary Decision Diagrams; Slides: 14-bdd.pdf Baier-Katoen, Sections 6.7.3 and 6.7.4
Class 15,
28 Oct 2019		 Guest lecture by Sergio Campos on compositional methods and case studies; Slides: campos-1-motivation.pdf, campos-2-compositional.pdf, campos-3-vod.pdf, campos-4-in-silico-exps.pdf
Class 16,
30 Oct 2019		 15. CTL model checking; Slides: 15-ctl-model-checking.pdf Baier-Katoen, Section 6.4
Class 17,
4 Nov 2019		 16. Automata: Finite automata; Omega automata; Buchi automata; Slides: 16-automata.pdf Baier-Katoen, Sections 4.1 and 4.3
Class 18,
6 Nov 2019		 17. LTL model checking; Slides: 17-ltl-model-checking.pdf Baier-Katoen, Section 5.2
Class 19,
13 Nov 2019		 Homework and exam review.
18. Bounded model checking; Slides: 18-bmc.pdf
Class 20,
18 Nov 2019		 19. Controller Synthesis: Slides: 19-controller-synthesis.pdf Alur-Tripakis SIGACT paper "Automatic Synthesis of Distributed Protocols",
Class 21,
20 Nov 2019		 20. Program Synthesis: Slides: 20-program-synthesis.pdf
Class 22,
25 Nov 2019		 21. Homework 4 exhibit; Parting thoughts. Slides: 99-bye.pdf
Class 23,
2 Dec 2019		 22. Project and paper presentations
Class 24,
4 Dec 2019		 23. Project and paper presentations

Logistics

Course structure

Biweekly lectures and homeworks. At the end of the semester, we will have student presentations (paper presentations by both undergraduate and graduate students; plus project presentations by graduate students).

Textbooks

We will not follow a specific textbook. However, the following textbooks are useful readings: More advanced reading:

Software

Install and familiarize yourself with:

Forum

We will use this piazza forum to post questions, answers, thoughts, links, etc, related to the course. Please check it at least every few days and participate actively. You can use it to post questions related to the projects or homeworks in this course. Specifically, clarification questions about the homework, such as "What does XYZ in homework 3 question 2.b mean?" should be posted to the forum. Also questions about the material covered lectures, e.g., "Is this LTL formula satisfied on this transition system? Why or why not?" should be posted to the forum.

Never be afraid to ask questions: ask in the forum, ask during class. Always remember: there are no stupid questions!

Homeworks

Homework assignments are posted on Blackboard. The assignments are to be done either individually or by groups of 2-3 students. To collaborate effectively, you should all be involved in all aspects of the homework problems. Homeworks will be marked 20 points off per day that they are late, up to 2 days. Important: You are responsible for finding a partner (e.g., using the piazza forum, or before/after lectures). Homework submission instructions will be made available in class. Any requests for grade changes or regrading must be made within 7 days of when the work was returned. To ask for a regrade, specify (a) the problem or problems you want to be regraded, and (b) for each of these problems, why you think the problem was misgraded.

Exams

There will be two exams. The first exam will be given approximately halfway through the semester and the second exam will be given towards the end of the semester. They will both be in-class exams.

Presentations

Every student will pick 1-2 relevant research papers that they find interesting and will read and present to the class. The presentation should include a motivation, it should relate the presented material to the material covered in class and it should explain why the topic is important and interesting. We will schedule the presentations later and determine their length and dates. The instructor will recommend some papers but students are encouraged to search and propose papers that they want to present themselves. Important: presentations are done individually, not in groups.

Projects

Projects are required only for graduate students. Graduate students have to propose a project that the instructor will review and approve (some suggestions will be provided by the instructor but as with presentations, students are encouraged to propose their own projects). Projects allow you to gain hands-on experience on a topic of interest. We suggest first choosing a project and then selecting papers for your presentation related to your project topic. Your project can be theoretical, say coming up with a verification or synthesis algorithm, or they can involve the implementation of an interesting algorithm, or they can involve the use and evaluation of existing tools (e.g., modeling and verifying some protocol).

Grading

Undergraduate students: Graduate students:

Academic Integrity

It's OK to ask someone about the concepts, algorithms, or approaches needed to do the assignments. We encourage you to do so; both giving and taking advice will help you to learn. However, what you turn in must be your own, or for projects, your group's own work; copying other people's code, solution sets, or from any other sources is strictly prohibited, unless you are explicitly given permission to do so. In particular, looking at other solutions (e.g., someone else's solution to a similar project) is a direct violation of our academic integrity policy. The project assignments must be entirely the work of the students turning them in. If you have any questions about using a particular resource, ask me. All students are subject to the Northeastern Academic Integrity policy. All cases of suspected plagiarism or other academic dishonesty will be referred to the Office of Student Conduct and Conflict Resolution (OSCCR) and to the college. In addition to any penalties imposed by OSSCR and the college, each violation of the academic integrity policy will result in a full grade reduction for the class in addition to a zero grade on any affected assignments, projects, exams or graded material.

Accommodations for Students with Disabilities

If you have a disability-related need for reasonable academic accommodations in this course and have not yet met with a Disability Specialist, please visit the Northeastern Disability Resource Center and follow the outlined procedure to request services. If the Disability Resource Center has formally approved you for an academic accommodation in this class, please present the instructor with your "Professor Notification Letter" during the first week of the semester, so that we can address your specific needs as early as possible.
Page maintained by Stavros Tripakis