Formal Methods for Cyber-Physical Systems

Syllabus:

Cyber-Physical Systems (CPS) are systems where a digital controllers interact with the external physical environment. Examples of CPS are control systems in avionics and automotive, and, more recently, autonomous systems using machine learning. CPS are complex to design, also for for the interaction of discrete software and the continuous-time behavior. Formal methods provide a set of mathematical techniques to precisely model and then analyze the correct behavior of CPS.

This course covers the basic of modeling and automatic formal verification for Cyber-Physical Systems (CPS), focusing on different kind of systems: discrete, continuous, and "ai-enabled" systems (mostly complex systems including neural networks) .

In the course, we will first focus on discrete systems, formally introducing transition systems as modeling language and model checking algorithms for safety verification. Then, we will study continuous-time systems, modeled with Ordinary Differential Equations (ODES), and set-based reachability analysis methods to show bounded-time safety. We will then see how we can extend both modeling and verification to mixed discrete-continuous systems (hybrid systems).

Finally, we will study some of the recent formal verification methods for autonomous systems using machine-learning components. We will look at the specific problem of robustness verification of neural networks and at the problem of verifying discrete-continuous systems that incorporate neural networks.

Acquired Competencies:

  - Formal modeling of Cyber-Physical Systems (discrete, concurrent, and continuous systems)
  - Verification (using model checking and reachability analysis) of safety for discrete and continuous systems
  - Hands-on experience on open-source verification tools
  - Verification of autonomous systems using machine-learning components (robustness, safety of closed-loop systems)

Pre-requisites:

  - Programming
  - Algorithms and data structure (standard graph algorithms like DFS, BFS)
  - Linear algebra
  - Calculus
  - Propositional and first-order logic

Evaluation

- 50% homework
- 50% individual project (30% project report, 20% project defense)

The students will have to individually complete a homework sheet with questions and exercises (both theoretical and practical) on the last 
week's topic. The students are required to submit their homework every week.

The students will be also evaluated on an individual project, requiring them to:
- apply existing formal methods technique to a medium-sized system; or
- implement and evaluate an existing verification algorithm.
We will provide a set of projects to the students.
The students will have to:
  - submit a written report and their source code and examples (when applicable); and
  - present their project (15' presentation + 10' questions).

Details of the classes (each class is 1.5h)

- Analysis of Discrete systems

 1. Introduction to Formal Method for CPS

 2. Verification for discrete systems (transition systems and reachability analysis)

 3. Introduction to temporal logics (LTL and CTL)

 4. Verification algorithms for CTL properties

 5. Bounded Model Checking for LTL properties

- Analysis of Hybrid Systems

 6. Continuous Time Systems - Modeling, Verification Problems, Challenges

 7. Verification of Continuous-Time Systems

 8. Hybrid Systems - Modeling, Verification Problems, Challenges

 9. Verification of Hybrid Systems

- Analysis of AI-enabled systems

10. AI-enabled Systems: Motivations and Verification Problems

11. Robustness verification for Feed-Forward Neural Networks (part 1)

12. Robustness verification for Feed-Forward Neural Networks (part 2)

13. Closed-loop verification for AI-enabled systems (closed-loop systems + neural networks)

14. Project discussion

Classes are held online at 4.20 pm every Tuesday starting from January, 25.

Click here to sign up