CDS 270
Home

CDS 270: Verification in Controls (Fall 2009)

This is the homepage of CDS 270 - Verification in Controls, Fall 2009.

CDS 270 - Verification in Controls is aimed at students interested in formal analysis of dynamical systems. Topics include verification concepts in controls such as stability, safety, and input-output properties. In the second half of the course, motivated by the challenges in cyber-physical systems, we will go beyond classical controls and discuss verification in the intersection of computer science and controls. Computational tools such as semidefinite programming and model checking will be emphasized. The course will include concrete motivating examples, hands-on exercises, and a project. Course Flier

Instructors:

Lectures:

Tuesdays and Fridays, 10:30am-noon
Steele Hall, room 214.

Course Description

  • 9 units (3-0-6)

  • Prerequisites: basic knowledge in controls (such as CDS 110).

  • Students will be asked to work on a term project.

Project

  • Proposal submission: October 23rd, midnight.

  • Final reports are due Dec 7th, midnight.

  • Time of oral presentations - TBD.

Homework Assignments

A short homework assignment will be handed out at each lecture. If you are taking the course for credit, you will be expected to submit your solutions in a week from the assignment date.

Slides & notes

  • Oct, 2 - Lecture 1 (includes a relatively better discussed list of topics to be covered in the course)

  • Oct, 6 - Lecture 2 (includes a detailed list of the topics to be covered during the lecture and a few important dates related to the projects)

  • Oct, 9 - Lecture 3 (Optimization problems and convex optimization problems (LP, QP, QCQP, SDP), introduction to duality.

  • Oct, 13 - Lecture 4 slides, Demo files m file, pdf file, and html file.

  • Oct, 16, - A list of topics and pointers to a few good references are here. The demo file is used to illustrate a few of the concepts covered in this lecture.

Starting from this lecture we will need two more matlab packages: multipoly and sosopt. These can be downloaded from this web site. Check the Matlab software part of that site. Remember to add these to your matlab path (this should be enough - no installation or anything).

Slides for Lecture 6 contain more than we can cover during in 90 minutes. We may discuss these at some point over the next few lectures or they are there for completeness.

  • Oct, 23 - Lecture 7 slides We will start with the material posted for the previous lecture and then continue with Lecture 7 slides.

Some (relatively old) references on nonlinear systems analysis and optimization-based (sum-of-squares optimization in specific) analysis are available here.

  • Oct, 30 - These slides are on ROA calculations with parametric uncertainties and these are on a case study on glycolysis dynamics.

The slides on the glycolysis dynamics are based on two recently submitted conference papers: First paper and second paper. In fact these two papers use ideas from a third (relatively older) paper.

  • Nov, 3 - First part of the lecture will cover the remaining parts of the slides on ROA calculations with parametric uncertainties. The second half will be an introduction to temporal verification. A good source for temporal verification using barrier certificates is available here. Later we will come back to temporal verification.

Guest Lecture: Prof. Eric Feron from Gatech will deliver an online guest lecture on Nov 3rd at 12:30pm. We will meet in Steele 110 for this lecture. Slides are here.

  • Nov, 6 - References: “Principles of Model Checking” by Christel Baier and Joost-Pieter Katoen. The basic terminology and results that we’ll cover can be found here in lecture slides from a short course by Katoen.

  • Nov, 13 - Notes on transition systems and linear time properties. These should be useful in assignment 7.

  • Nov, 18 - Example files used by Nok for the TLA-TLC demonstration are now available. More background information on TLA is available here.

  • Nov, 21 - Notes on regular languages, regular safety, regular properties, and linear temporal logic. These should be useful in assignment 8.