Home
Administrivia
Overview
Schedule
Problem Sets
Resources
| Date | Topic | Lecture Notes (scribed by) | Others | |
|---|---|---|---|---|
| L1 | Tue 08/26 | Motivation, challenges, examples in modeling and verification | .pdf (Taylor J.) | Project ideas handed out |
| L2 | Thu 08/28 | Modeling: discrete time, asynchronous, distributed systems | .pdf (John S.) | |
| L3 | Tue 09/02 | Modeling real-time and hybrid systems I | .pdf (Arefin M.) | PS1 out |
| L4 | Thu 09/04 | Modeling real-time and hybrid systems II | .pdf (Vladimeros V.) | |
| L5 | Tue 09/09 | Specifying properties of finite state models: LTL | .pdf (Ryan K.) |
| Date | Topic | Lecture Notes | Others | |
|---|---|---|---|---|
| L6 | Thu 09/11 | CTL and explicit state model checking | .pdf (Candido S.) | |
| L7 | Tue 09/16 | CTL model checking continued, OBDDs | .pdf (Kyoung-Dae) | PS1 due |
| L8 | Thu 09/18 | Symbolic Model Checking (of finite state models) | .pdf (Kyoung-Dae) | PS2 out |
| L9 | Tue 09/23 | Integral Timed Automata | .pdf .tex | Project proposals due |
| L10 | Tue 09/30 | TCTL and UPPAAL tutorial | .pdf .tex | UPPAAL files Failure detector spec query Switch spec |
| L11 | Thu 10/02 | Model Checking Timed Automata: Region Construction | .pdf (Aneel T.) | |
| L12 | Tue 10/07 | Rectangular Hybrid Automata | .pdf .tex | PS2 due |
| L13 | Thu 10/09 | Undecidability of non-initialized rectangular HA | .pdf (Amin S.) | PS3 out |
| L14 | Tue 10/14 | A class of decidable Hybrid systems: planar-linear HA | slides paper | Guest lecturer: Pavithra Prabhakar |
| L15 | Thu 10/16 | Implementing real-time/embedded systems: Time-triggered Approach | slides | |
| L16 | Tue 10/21 | Deductive verification: PVS | slides | |
| L17 | Thu 10/23 | PVS Part 2 | slides (same as above) PVS files for min problem. | PS3 due. Exercise: model a stack in PVS & prove properties stated in class. |
| L18 | Tue 10/28 | Implementation and Simulation | .pdf (Arefin) | |
| L19 | Thu 10/30 | Predicate abstraction for Hybrid Systems | .pdf .tex | |
| L20 | Tue 11/04 | Counterexample guided abstraction/refinement | .pdf .tex | |
| L21 | Thu 11/06 | Stability verification: Multiple Lyapunov functions | .pdf .tex | PS4 out |
| L22 | Tue 11/11 | Stability verification: Slow switching, dwell time, abstractions | .pdf .tex |
| Date | Topic | Lecture Notes | Others | |
|---|---|---|---|---|
| L23 | Thu 11/13 | Path planning with hybrid controllers | ||
| L24 | Tue 11/18 | Compositional and assume guarantee reasoning | ||
| L25 | Thu 11/20 | Applications in biology and Wrap-up | Draft of project reports due on 23rd. | |
| P1 | Project presentations I | |||
| P2 | Project presentations II |
| Date | Project title | Members | |
|---|---|---|---|
| P1 | Tue 12/02 11:00-11:16am | SWARM: Software Automata for Robotic Motion | Arefin & John |
| P1 | Tue 12/02 11:18-11:34am | STORMED Hybrid Systems and Games .pdf slides | Vlad |
| P1 | Tue 12/02 11:36-11:52am | TIOA2PHAver Conversion Tool | Amin & Vijay Anand |
| P1 | Tue 12/02 11:54-12:10pm | Programming Bi-Ped Robot with HIOA .ppt slides | Chris |
| P2 | Thu 12/02 11:00-11:16am | Output Generation by Switched Systems using Invertibility .ppt slides | Aneel |
| P2 | Thu 12/02 11:18-11:34am | Robot Coordination and Verification .ppt slides | Ryan & Juan |
| P2 | Thu 12/02 11:36-11:52am | Stability Analysis of Simplex Architecture: Controlled Inverted Pendulum .pdf slides | Taylor |
| P2 | Thu 12/02 11:54-12:10am | Stability Analysis of Distributed Vehicle Control System .ppt slides | Kyoung-Dae |
| P2 | Thu 12/02 12:12-12:28am | Reachability Analysis of Robotic Motion Planning .pdf slides | Sal |