CSCI 5854: Foundations of Cyber-Physical Systems


*Image inspired by Lee and Seshia (http://leeseshia.org/).

Logistics


Relevant Textbooks



Assignments


Grading

The overall grade will be based on a cumulative score computed by adding together the grades from:

Topics Covered

  1. Mathematical Models of Systems and Their Properties
    • Synchronous Discrete Models: (Extended) Finite State Machines (FSMs)
    • Asynchronous Models: Network of FSMs and Synchronization
    • Continuous Time Models: Ordinary Differential Equations
    • Hybrid Models: Timed Automata, Multi-mode Systems, and Hybrid Automata
    • Probabilistic Models: Markov Decision Processes and Probabilistic Timed Automata (*)
  2. Requirement Specification Formalisms
    • Specification Types: Safety, Liveness, Reactivity, Stability
    • omega-automata and temporal logics (LTL and MTL)
  3. Verification Techniques
    • Model Checking
    • Deductive Verification: Lyapunov and Barrier Certificates
    • Simulation-Based Verification: RRTs and S-Taliro.
  4. Verification Tools
    • NuXMV model checker for discrete systems
    • UPPAAL model checker for timed systems
    • PRISM model checker for probabilistic systems (*)
    • S-TaLiRo: temporal logic falsification tool
    • Flow-star : a verification tool for hybrid systems
  5. Applications (*)
    • Real-Time Scheduling
    • Medical Devices (Artificial Pacemaker and Artificial Pancreas)
    • Robot Motion and Path Planning
    • Automotive Systems
Topics marked with (*) will be explored via student projects and presentations.

Schedule and Lecture Notes

The schedule of lectures shown below is subject to change. We will post lecture notes or provide pointers to the texbook. We will strive to post all material well in advance. Please take a look through them, and come prepared for class.
# Date Description Chapter
1 Week 1 —January 17 Cyber-Physical Systems: Introduction Alur (Chapter 1)

Part One: Discrete Dynamical Systems

2 Week 2 — January 22 Transition Systems and Extended Finite state machines (An informal introduction) Alur (Chapter 2)
3 Week 2 — January 24 Nondeterministic models. Alur (Chapter 2)
4 Week 3 — January 29 Composition, Events and Communication between models. class notes
5 Week 3 — January 31 Safety Verification: Overview of Model Checking
6 Week 4 — February 5 Demo of NuXMV. Introduction to SAT/SMT solvers
7 Week 4 — February 7 Bounded model checking for reachability
8 Week 5 — February 12 Beyond Safety: Liveness
9 Week 5 — February 14 Temporal Logic and omega automata
10 Week 6 — February 19 Model-Checking Temporal Logic
11 Week 6 — February 21 In-Class Quiz I

Part Two: Continuous Dynamical Systems

12 Week 7 — February 26 Continuous systems. Ordinary Differential Equations
13 Week 7 — February 28 Basic theory of ODEs. Existence and Uniqueness
14 Week 8 — March 5 Simulation of ODEs in Simulink(tm)
15 Week 8 — March 7 Linear ODEs and introduction to feedback control
16 Week 9 — March 12 Linear systems: reachability and stability
17 Week 9 — March 14 Eigenvalues, pole placement, introduction to PID control
18 Week 10 — March 19 Stability Analysis: Lyapunov Functions and Barrier Certificates
19 Week 10 — March 21 In-class Quiz II
21 Week 11 — March 26-30 No Class — Spring Break

Part Three: Hybrid Dynamical Systems

20 Week 12 — April 2 Hybrid Systems: Basic introduction and examples
22 Week 12 — April 4 Hybrid automata: Theoretical Results
23 Week 13 — April 9 Hybrid Automata: Simulations using Simulink/Stateflow
24 Week 13 — April 11 Hybrid Automata: Metric Temporal Logic, Robustness, and Falsification
25 Week 14 — April 16 Hybrid Automata: Bounded Model Checking, Flowpipe construction, Flowstar tool demo
26 Week 14 — April 18 Timed Automata: Theory and tool demo
28 Week 15 — April 23 Probabilistic Modeling: Verification and PRISM tool demo

Part Four: Applications

29 Week 15 — April 25 Applications I (TBA)
30 Week 16 — April 30 Applications II (TBA)
31 Week 16 — May 2 Applications III (TBA)

Notes

  1. Accommodation Statement. If you qualify for accommodations because of a disability, please submit to me a letter from Disability Services in a timely manner (for exam accommodations provide your letter at least one week prior to the exam) so that your needs can be addressed. Disability Services determines accommodations based on documented disabilities. Contact Disability Services at 303-492-8671 or by e-mail at dsinfo [AT] colorado.edu. If you have a temporary medical condition or injury, see Temporary Injuries under Quick Links at the Disability Services website and discuss your needs with me.
  2. Religious Observances. Campus policy regarding religious observances requires that faculty make every effort to deal reasonably and fairly with all students who, because of religious obligations, have conflicts with scheduled exams, assignments or required attendance. In this class, you should notify your instructor of any conflict at least two weeks in advance. See full details here .
  3. Classroom Behavior. Students and faculty each have responsibility for maintaining an appropriate learning environment. Those who fail to adhere to such behavioral standards may be subject to discipline. Professional courtesy and sensitivity are especially important with respect to individuals and topics dealing with differences of race, color, culture, religion, creed, politics, veteran's status, sexual orientation, gender, gender identity and gender expression, age, disability, and nationalities. Class rosters are provided to the instructor with the student's legal name. I will gladly honor your request to address you by an alternate name or gender pronoun. Please advise me of this preference early in the semester so that I may make appropriate changes to my records. For more information, see the policies on classroom behavior and the student code.
  4. Discrimination and Harassment. The University of Colorado Boulder (CU Boulder) is committed to maintaining a positive learning, working, and living environment. CU Boulder will not tolerate acts of sexual misconduct, discrimination, harassment or related retaliation against or by any employee or student. CU's Sexual Misconduct Policy prohibits sexual assault, sexual exploitation, sexual harassment, intimate partner abuse (dating or domestic violence), stalking or related retaliation. CU Boulder's Discrimination and Harassment Policy prohibits discrimination, harassment or related retaliation based on race, color, national origin, sex, pregnancy, age, disability, creed, religion, sexual orientation, gender identity, gender expression, veteran status, political affiliation or political philosophy. Individuals who believe they have been subject to misconduct under either policy should contact the Office of Institutional Equity and Compliance (OIEC) at 303-492-2127. Information about the OIEC, the above referenced policies, and the campus resources available to assist individuals regarding sexual misconduct, discrimination, harassment or related retaliation can be found at the OIEC website.
  5. Honor Code. All students enrolled in a University of Colorado Boulder course are responsible for knowing and adhering to the academic integrity policy of the institution. Violations of the policy may include: plagiarism, cheating, fabrication, lying, bribery, threat, unauthorized access, clicker fraud, resubmission, and aiding academic dishonesty. All incidents of academic misconduct will be reported to the Honor Code Council (honor@colorado.edu; 303-735-2273). Students who are found responsible for violating the academic integrity policy will be subject to nonacademic sanctions from the Honor Code Council as well as academic sanctions from the faculty member. Additional information regarding the academic integrity policy can be found at honorcode.colorado.edu.
  6. The web-page of a previous offering of the course is available here and here .