CS 591, Formal Modelling and Analysis of Cyber-Physical Systems

 Monsoon 2021-2022

Instructor 

  1. S. Ramesh (GM R&D, Warren, Michigan and Adjunct Professor, IITG), Email: ramesh.s

  2. Purandar Bhaduri, Email: pbhaduri

Teaching Assistant

Manish Semwal  (Email: smanish)

Class Schedule

Time: 5:00 - 5:55 PM,  Days: Wed, Thu, Fri

Course Contents

Textbook

Sayan Mitra, Verifying Cyber-Physical systems, MIT Press, 2021.

References

  1. Rajeev Alur, Principles of Cyber-Physical Systems, MIT Press, 2015.
  2. Edward A. Lee and Sanjit A. Seshia, Introduction to Embedded Systems, A Cyber-Physical Systems Approach, MIT Press, 2017. (You can download a pdf version from the above site).

Slides from similar courses

  1. Slides and Code by Sayan Mitra (UIUC) accompanying the textbook.

  2. ECE/CS 584: Formal Verification of Embedded & Cyberphysical Systems, Spring 2016, UIUC course slides by Sayan Mitra

  3. ECE/CS 584: Embedded & Cyberphysical System Verification, Fall 2021, UIUC course slides by Sayan Mitra.

  4. Lectures by Sayan Mitra in GIAN Course on Modeling and Verification of Cyber-Physical Systems, IIT Guwahati, January 1-5, 2018.

  5. Course on Foundations of Embedded Systems by Cesare Tinelli at Iowa. Chapters 6, 7 and 9 are relevant for this course.

  6. Course on Autonomous Cyber-Physical Systems by Jyotirmoy Deshmukh at USC (with lecture slides)

  7. Course on Cyber-Physical Systems by Laura Nenzi at Trieste (with lecture slides).
     

Other useful resources (freely available from the net)

  1. Karl J. Åström and Richard M. Murray, Feedback Systems: An Introduction for Scientists and Engineers, Second edition, Princeton University Press, 2021. (Chapters 3, 5 and 6 are helpful for this course as background material).

  2. Lecture Notes on Foundations of Cyber-Physical Systems, André Platzer, Carnegie Mellon University.

  3. Lecture Notes on Hybrid Systems by John Lygeros.

  4. Notes on Lyapunov's theorem by Federico A. Ramponi.

Tutorial, Survey Papers and Lecture Slides on Formal Verification

  1. Linear-Time Temporal Logic and Büchi Automata, Tutorial talk by Madhavan Mukund, Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, January 1997. 

  2. Finite-state Automata on Infinite Inputs, Madhavan Mukund, Modern Applications of Automata Theory, World Scientific (2012) 257-288.  

  3. Model-checking: Automated Verification of Computational Systems, Madhavan Mukund, Resonance, July 2009.

  4. Model Checking, Edmund M. Clarke, Bernd-Holger Schlingloff, Handbook of Automated Reasoning 2001.

  5. Satisfiability Modulo Theories, Clark W. Barrett and Cesare Tinelli, in Handbook of Model Checking, (Ed Clarke, Thomas Henzinger, and Helmut Veith, eds.), 2017.

  6. Satisfiability modulo theories: introduction and applications, Leonardo de Moura and Nikolaj Bjørner, CACM Vol 54, Issue 9, 2011.

  7. Course on Introduction to Model Checking by Joost-Pieter Katoen at Aachen, with lecture slides.

  8. Course on Automated reasoning and program verification by Ashutosh Gupta at IIT Bombay, with lecture slides.

  9. Course on Automated Program Verification by Kartik Nagar at IIT Madras, with lecture slides.

  10. Course on Program Verification by Christoph Matheja and Peter Müller at ETH Zurich, with lecture slides.
     

 

Tools

  1. Matlab / Simulink (Download Matlab from here.)

  2. SpaceEx

  3. dReal and dReach

  4. FLOW*

  5. CORA

  6. UPPAAL

  7. C2E2

  8. KeYmaera X

Tutorials

  1. Matlab and Simulink tutorials from MathWorks

Benchmarks and Case Studies

  1. Benchmarks of continuous and hybrid systems

  2. A Benchmark Suite for Hybrid Systems Reachability Analysis by X. Chen at al, NASA Formal Methods Symposium
    NFM 2015.

     

Evaluation

Seminar, Term Paper and Mini-Project    50%

Quizzes and Exams                                  50%

 

 

 back to homepage