Verification of Embedded and Cyberphysical systems
Verification is the art and science of establishing that a given system meets a given set of requirements. For example, an assertion such as “an adaptive cruise control system in a car does not lead to any collisions.”
Cyberphysical systems (CPS) Links to an external site. combine software components with sensors, actuators & communication. From driverless cars to air-traffic control systems, medical devices to manufacturing robots, many new and old engineering systems fit the description of what are now called cyberphysical systems.
Many CPS systems are mission-critical, so verification is essential for their applications. In particular, the use of machine learning and AI in these systems will make the verification of these systems even more challenging.
In this course, you will:
- Learn to create mathematical models of cyberphysical systems
- Learn the fundamental principles of verification
- Gain experience in using powerful verification tools (model checkers Links to an external site., SMT solvers Links to an external site., theorem provers Links to an external site., and neural network verifiers Links to an external site.)
- Read and discuss recent ideas from research papers
- Gain in experience in formulating research problems in the area of cyberphysical systems/formal verification. This course especially highlights the recent developments in the formal verification of machine-learning (ML) and AI enabled systems.
Instructor: Prof. Huan Zhang
Links to an external site. (huanz at illinois dot edu)
Teaching assistant: Keyi Shen (keyis2 at illinois dot edu)
Canvas (for homework submission): https://canvas.illinois.edu/courses/56512
Please use the course website https://publish.illinois.edu/ece584-spring2025/ for latest course schedule and slides. Canvas is used for class announcements and homework assignments only.
Book
The course will largely follow the textbook by Prof. Sayan Mitra, with additional components on the verification of machine learning enabled systems. Additional readings may be assigned before each lecture.
Verifying cyberphysical systems, by Sayan Mitra, published by MIT Press, 2021. Supplementary materials are available from here Links to an external site..
Lectures
Time: Tuesday and Thursday 11:00AM – 12:20PM
Location: 3015 Electrical & Computer Eng Bldg (ECEB)
Zoom (for UIUC online MS Eng students only): https://illinois.zoom.us/j/89423827505?pwd=yszhKhjHU4985RTNUze0N1DkJ0KNjL.1
Links to an external site. (Passcode: 818094)
You will be required to do the assigned reading from the above book draft ahead of time. The lectures will not repeat the same topics but provide a complementary view of the material in the book.
Grading
- Homework (4 sets): 40%
- Problems will involve some coding and pencil paper proofs
-
- Project: 55%
- Proposal: 10%
- Midterm presentation: 10%
- Final presentation (EOS): 15%
- Report (EOS), code and documentation: 20%
- Participation: 5%
- Provide feedback on peer projects
- Class participation, new problem suggestions and solutions
Important Dates:
- Project Proposal due: check "assignments" for due date
- Midterm presentation (5 mins): Week after Spring break
- Final presentations: Last week of instruction
- Final report: Due final’s week
Homework
There will be 4 sets of individual homework. The homework problems will involve pencil-paper proofs and some coding. The homework will be concentrated on the earlier 2/3rd of the semester.
Homework submission: homework needs to be submitted on Canvas. Submissions through other channels will not be accepted. Homework will be due at 11:59 pm CT on the due date.
Late policy: for each late day, there will be a 20% penalty on your grade. After 5 days, late homework will not be accepted. For example, if you submitted your homework two days late and scored 90, your grade for this late homework will be 90*60%=54. For medical excuses, please email me your absence letter from the Office of the Dean of Students.