Foundations of Formal Methods and Cyber-Physical Systems (CS522) Spring 2024

Instructor:

Vinayak Prabhu
Office: 446 Computer Science Building
Office hours: After Class, and by appointment
Email:

Course Description:

• This course will cover formal methods based techniques for the design, correctness specification, and analysis of cyber-physical systems (CPS). CPS are integrations of control software, physical sensors and physical hardware in which software continuously reacts to sensor data and/or issues commands to physical actuators. Such systems are becoming ubiquitous, from self-driving cars to smart buildings.
  The CPS page at the National Science Foundation.
  Formal methods for our purposes, are principled approaches to system modeling, specification, design, analysis, verification, and synthesis. While we will apply these techniques in lectures to CPS, the same techniques are also used for rigorous reasoning, often with automated tools, about the correctness of reactive software systems. Our focus will be on precision in formulating problems and objectives (rather than on proofs).
  Formal methods are now used in most major software companies.
  How Amazon Web Services uses formal methods.
  Automated reasoning at Amazon

Textbooks:

• (Required) Principles of Cyber-Physical Systems, Rajeev Alur
• (Reference) Mathematical Structures for Computer Science by Judith L. Gersting (7th edition).
  This book is good for the CS220 background we will need. Sections from the textbook from the first chapter on Propositional and Predicate logic will be placed on electronic reserve.
• (Reference) Principles of Model Checking, Christel Baier and Joost-Pieter Katoen
• (Reference) Model Checking, Second Edition, Edmund M. Clarke, Jr., Orna Grumberg, Daniel Kroening, Doron Peled and Helmut Veith
• (Reference) Modern Control Systems, Richard C. Dorf and Robert H. Bishop

Prerequisites:

• Note: CS522 is independent of CS422/CS580A7.
  I will assume students are willing to spend time learning/refreshing missing or forgotten basic background material, such as propositional logic reasoning from CS220. The first couple of chapters in the main textbook give a good idea about the level of the course. If you have taken any of CS320 (Algorithms), ECE 311 (Linear Systems), CS422 (Automata, Logic, and Computation), or equivalent, you will be fine. A background in theory/algorithms/control systems will NOT be assumed (but will be helpful to have).
  In order to help you with CS 220 background material on logic and reasoning, I will provide a couple of sections from a CS220 text in the electronic reserve. Additionally, problems from these topics (propositional and predicate logic) will appear in homeworks and exams, enabling you to practice and develop active skills in these core areas. We will also discuss sticking points in lectures.


• Undergraduate students: Undergraduate students who have a B or better in any of CS422/CS420/ECE411/Math366 or similar courses are well prepared for this class and are welcome to take it (please contact me for an override). For other undergraduate students, overrides will be given on a case by case basis.

Lectures:

• Tuesday, Thursday, 5:30pm-6:45pm, Computer Science Building 130.
  With the permission of all the registered students (in case there are no clashes with other classes), we will move the class to 5:00pm-6:15pm. Students will be polled after the start of the semester.

Grading:

• Homework assignments, roughly seven. (weight 25%)
• Midterm exam I (CS220 material on propositional and predicate logic) in March. (weight 10%)
• Midterm exam II (open book) in April. (weight 30%)
• Term Project. (weight 35%)
  The project can be as follows depending on your choosing.
  • A survey/research project in some depth on an advanced topic related to the class, including application of formal methods concepts to the domain of your interest.
  • Working with a verification/testing tool on models.
  • Applications: CPS, autonomous systems (safe AI/safe ML), robotics and path planning, systems biology, medical devices, logic and decision procedures, testing, security.
  Deliverables:
  1. A written project proposal (in latex).
  2. A written project update report (in latex).
  3. Final project presentation.
  4. Final written project report (in latex).

Topics:

• Core logical reasoning techniques
• Propositional logic.
• Predicate logic.
• Mathematical Models of Systems
• Synchronous and Asynchronous models.
• Finite state machines.
• Continuous and discrete-time time models: Linear systems.
• Hybrid models: timed and hybrid automata.
• Property Specifications
• Safety, Liveness, Reactivity, Stability.
• Omega automata and temporal logics (LTL, STL).
• Verification, Testing, and Analysis Techniques
• Abstraction, refinement, CEGAR.
• Composition of models.
• Model-checking.
• Symbolic algorithms.
• SAT/SMT.
• Optimization based testing.
• Control
• Transient and steady-state behavior of linear systems.
• Laplace and Z-Transforms.
• Transfer functions, block diagrams, eigenvalues, poles and zeroes.
• Model order reduction.
• Stability analysis.

Homework and Readings:

• Written homework will be regularly assigned (posted on Canvas) and you will be expected to solve the problems. You are also expected to read the relevant sections from the textbook.
  Note: Posted lecture notes are not a substitute for textbook readings.