CS620: New Trends in Information Technology
Modeling and Analysis of Cyber-Physical Systems


Logistics


Relevant Textbooks


Grading


Topics

Part I: Formal Modeling

  1. Modeling and verification of discrete systems:
  2. Modeling timed systems
  3. Some generalizations of timed automata and their decision problems
  4. Introduction to hybrid automata

[Mid-semester Exams]

Part II: Tools for Modeling for Cyber-Physical Systems

  1. Timed model-checker UPPAAL
  2. Hybrid model-checker HyTech
  3. Stateflow/Simulink

Part III: Verification and Synthesis

  1. Specification of properties of timed systems
  2. Coping with undecidability: time-bounded verication
  3. Automatic Synthesis

[End-semester Exams]


Schedule and Lecture Notes

Date Description References/Lecture Notes
July 24 Introduction to cyber-physical systems modeling and verification [Slides ]
July 26 Green Sheduling and Multi-mode Systems [Slides] Green scheduling, Constant-rate Multi-mode systems
July 31 Green Sheduling and Multi-mode Systems (Contd.) [Slides] Green scheduling, Constant-rate Multi-mode systems
August 2 Extended Finite State Machines [Slides] class notes and lecture ntoes by Lygeros, Tomlin, and Sastry
August 7 Continuous Dynamical System [Slides] class notes and lecture ntoes by Lygeros, Tomlin, and Sastry
August 9 Institute Holiday
August 14 Hybrid Automata: Syntax, Semantics, and Examples [Slides] class notes and lecture ntoes by Lygeros, Tomlin, and Sastry
August 16 Timed Automata: Syntax, Semantics, and Examples A theory of timed automata
August 21 Guest lecture by Krishna S. region construction and temporal logic LTL/CTL
August 23 Class cancelled due to FORMATS'13 conference
August 28 Introduction to SPIN model-checker by Ganesh K. Narwane SPIN website and a Tutorial
August 30 Introduction to UPPAAL model checker by Ganesh K. Narwane and Devendra Bhave UPPAAL website and a tutorial.
September 4 Language Theoretic Properties of Timed Automata: finite automata closure, determinization, and alternation [Slides] J. E. Hopcroft, R. Motwani and J. D. Ullman. Introduction to Automata Theory, Languages and Computation
September 6 Language-theoretic Properties of Timed Automata: closure under union, intersection, and decidability of emptiness problem via region construction [Slides] Alur and Dill' 94, Chapter 9 of "Principles of Model Checking" book by Baier and Katoen, Chapter 6 from principles of embedded computation by Rajeev Alur.
September 11 No class due to Mid-semester exams
September 13 No class due to Mid-semester exams
September 16 Quiz 1
September 18 Timed Automata: properties and determinizability (lecture notes first and second by B. Srivathsan) Alur and Dill' 94, Chapter 9 of "Principles of Model Checking" book by Baier and Katoen, Chapter 6 from principles of embedded computation by Rajeev Alur, and Event-Clock Automata .
September 20 Class merged with the talk by Ansuman Banerje on Counterexample Ranking Using Mined Invariants (Venue: SIC 205, 'C' Block, 02nd Floor from 12noon)
September 25 Abstractions for Timed Automata (guest lecture by B. Srivathsan) slides

Additional Reading


Notes