Verification and Synthesis for Cyberphysical Systems (Fall 2015), ASE 396 & CS 395T
From u-t-autonomous.info
Revision as of 15:39, 3 January 2016 by Utopcu (Talk | contribs) (Undo revision 258 by Utopcu (talk))
Time: Tue & Thu 2-3:30pm
Room: WRW 413
Instructor: Ufuk Topcu, email
Office hours: By appointment.
Course description (ASE 396 & CS 395T, Fall 2015)
Announcements
- HW6 is posted. Consider the effective date of posting as 11:59pm on Dec 1st.
- HW4 is posted. Consider the effective date of posting as 11:59pm on Nov 4th.
- HW3 is posted. Consider the effective date of posting as 11:59pm on Oct 25th.
- HW2' (2prime !) is posted. Consider the effective date of posting as 11:59pm on Oct 8th.
- Project presentation slides (single pdf!) are due by noon on Oct 6th.
- HW2 is posted. Consider the effective date of posting as 11:59pm on Oct 4th.
- HW1 is posted. Due to the delay in the posting, consider the effective date of posting as Sept 15th.
- Every student is required to have met with the instructor to discuss his/her project plans by Sept 16th, 6pm. Email the instructor to schedule a meeting.
Schedule
| Date | Subject | Notes | Assignments | |
|---|---|---|---|---|
| 1 | Aug 27 | Logistics, intro and overview | slides | |
| 2 | Sep 1 | Modeling & finite transition systems | slides | |
| 3 | Sep 3 | No class | cancelled | |
| 4 | Sep 8 | Specifications (1) -- linear-time properties | slides | |
| 5 | Sep 10 | Specifications (2) -- automata-based representations | slides | |
| 6 | Sep 15 | Specifications (3) -- temporal logic | slides | HW 1 |
| 7 | Sep 17 | Model checking (1) | slides | |
| 8 | Sep 22 | Model checking (2) & closed-system synthesis | slides | |
| 9 | Sep 24 | Closed-system synthesis & demo | EC2 instructions | |
| 10 | Sep 29 | Probabilistic verification (1) -- DTMCs | slides | |
| 11 | Oct 1 | Probabilistic verification (2) -- MDPs | slides | HW 2 |
| 12 | Oct 6 | Project presentations (1) | ||
| 13 | Oct 8 | Open-system synthesis (1) | slides | HW 2' |
| 14 | Oct 13 | Open-system synthesis (2) | slides | |
| 15 | Oct 15 | Open-system synthesis (3) | slides (con't) | |
| 16 | Oct 20 | In-class, hands-on exercises | slides (con't), TuLiP on EC2, synthesis examples | |
| 17 | Oct 22 | Hybrid systems -- modeling & overview | slides | HW 3 |
| 18 | Oct 27 | Abstraction-based verification | slides | |
| 19 | Oct 29 | Abstraction-based control (1) | slides | |
| 20 | Nov 3 | Abstraction-based control (2) | slides (con't) | HW 4 |
| 21 | Nov 5 | Abstraction-based control (3) | slides (con't) | |
| 22 | Nov 10 | Techniques for scaling | slides | |
| 23 | Nov 12 | Optimization primer | slides | |
| 24 | Nov 13 | Project presentations (2) | ||
| 25 | Nov 19 | Deductive verification (1) | slides | HW 5 |
| 26 | Nov 24 | Deductive verification (2) | slides | |
| 27 | Dec 1 | Deductive verification (3) | slides (con't) | HW 6, mat file |
| 28 | Dec 3 | Deductive verification (4) | slides |
Corrections to be made in the slides
Homework assignments
- Each assignment is due in 10 days from the day it is posted (not counting the day on which it was posted). For example, an assignment that is posted on Sept 24th is due on Oct 4t @ 11:59pm.
- Each student is supposed to email all his/her work in a single pdf to utopcu@utexas.edu. If the assignment involves programming, then accompanying code should be attached as well.
Projects
Type of the project: The choice of the project topics is flexible. Application of existing techniques to a new problem (e.g., from your own research), software implementation and benchmarking of an existing algorithm and extension of an existing algorithm are all good projects.
Topic of the project: If you have a topic in mind, feel free to discuss with the instructor as soon as possible. Alternatively, here are some potential project topics.
Reporting: Two short presentations (during the semester) for progress report and a final report are required. The progress report will be a single slide in a GOTChA-chart style (see the link for GOTChA charts).
- Progress report and short presentation (1) -- See the schedule for the presentation day. The pdf version of the single slide is to be turned in by 9am on the day of presentations by email. The chart should clearly state the plans until the second presentation day.
- Progress report and short presentation (2) -- See the schedule for the presentation day. The pdf version of the single slide is to be turned in by 9am on the day of presentations by email. The chart should be modified to reflect on the accomplishments so far and plans for the rest of the semester.
- Final report -- Due 11:59pm on the official day of the final exam for the course.
Notes
- A Roadmap for U.S. Robotics: From Internet to Robotics, 2013 Edition
- CPS Virtual Organization
- Principles of Model Checking (Baier and Katoen) (UT Library entry)
- NuSMV model checker, tutorial
- Instructions to access the EC2 instances and to run NuSMV
- PRISM (probabilistic verification tool
- Katoen's tutorial slides on probabilistic verification at CAV '15: part 1, part 2, part 3, part 4
