Introduction to Embedded Systems Lee Seshia Solution Manual
Verification and Control of Cyber-Physical Systems (CSCI 7000, Fall 2014)
Course Information
-
Class Timings: Tuesday-Thursday 9:30-10:45 AM
-
Class Location: ECCR 139
-
Instructor: Sriram Sankaranarayanan
-
Pre-Requisites: Background in Embedded Systems or Control Theory. Undergraduate Level Calculus and some exposure to CS theory.
-
Office Hours: Wednesdays 12-1 PM and Thursdays 1-2PM ECOT 624.
News
-
Watch this space for important announcements.
Assignments
Assignments will be posted here.
-
Assignment # 1 (Due on Thursday, September 11, 2014).
-
Solutions
-
-
Assignment # 2 (Due on Thursday, September 18, 2014).
-
Solutions
-
-
Assignment # 3 (Due on Thursday, October 2, 2014).
-
Solutions
-
-
Assignment # 4 (Due on Thursday, October 22, 2014).
-
Solutions
-
-
Assignment # 5 (Due on Tuesday, November 4, 2014).
-
Solutions and ZIP file for matlab scripts and simulink diagrams.
-
-
Assignment # 6 (Due on Tuesday, December 4, 2014).
Lecture Schedule and Notes
The schedule of lectures shown below is subject to change. We will post lecture notes for most topics and videos for selected topics. We will strive to post all material well in advance. Please take a look through them, and come prepared for class.
ID | Date | Topics Covered | Book Sections | |
1 | Aug 26th | Introduction to Cyber-Physical Systems | ||
2 | Aug 28th | Motivating Examples. Modeling, Design and Verification. Hierarchy of CPS models. | Alur-Ch1 | |
3 | Sep 2nd | Synchronous Models: Introduction and Examples | Alur-Ch2 | |
4 | Sep 4th | Synchronous Models: Sequential and Parallel Composition | ||
5 | Sep 9th | Guest Lecture (Prof. Cerny): Transition Systems and Safety Verification | Alur-Ch3 | |
6 | Sep 11th | Safety Properties, State-Space Exploration, On-The-Fly Model Checking | ||
7 | Sep 16th | Safety Properties: Symbolic Model Checking | ||
8 | Sep 18th | Safety Verification: Symbolic Search | ||
9 | Sep 23rd | Z3 tutorial, Invariants, Invariant Verification | ||
10 | Sep 25th | Invariant Verification, Bounded Model Checking | ||
11 | Sep 30th | Beyond Safety: Liveness | Alur-Ch5 | |
12 | Oct 2nd | Temporal Logic and omega automata | Alur-Ch5 | |
13 | Oct 7th | Model Checking Temporal Logic | Alur-Ch5 | |
14 | Oct 9th | Ordinary Differential Equations (Guest Lecture Amin) | Alur-Ch6 | |
15 | Oct 14th | Ordinary Differential Equations (Guest Lecture Amin) | ||
16 | Oct 16th | Ordinary Differential Equations (Guest Lecture Amin) | ||
17 | Oct 21st | Eigenvalues, pole placement, introduction to PID control | ||
18 | Oct 23rd | Simulation of ODEs in Simulink(tm) | ||
19 | Oct 28th | Simulation with Simulink + Specifications for Continuous Systems | ||
20 | Oct 30th | ODEs, Lipschitz continuity: existence of solutions, equilibria, Stability criteria | ||
21 | Nov 4th | Stability Analysis: Lyapunov Functions and Barrier Certificates | Alur - Ch 6 Complete | |
Nov 6th | Quiz on first half of the class | |||
23 | Nov 11th | Hybrid Systems: Basic introduction and examples | Alur - Ch 9 | |
24 | Nov 13th | Hybrid automata: definition of trajectories, zenoness | ||
25 | Nov 18th | Simulations using Simulink/Stateflow, Temporal Logics for Continuous Time | ||
26 | Nov 20th | S-Taliro: Robustness guided falsification of hybrid systems | ||
27 | Dec 2nd | Flowpipe construction: Flowstar tool demo | ||
28 | Dec 4th | Applications Lecture: Artificial Pancreas Control |
Syllabus (Topics Covered)
Topics Covered
-
Mathematical Models of Systems and Their Properties
-
Structure of Feedback Control Systems: Hands-On Introduction
-
Continuous Time Models: Ordinary Differential Equations.
-
Synchronous Discrete Models: Finite State Machines
-
Asynchronous Models: Network of Automata and Synchronization.
-
Timed and Hybrid Models.
-
-
Property Specifications
-
Specification Types: Safety, Liveness, Reactivity, Stability.
-
-automata and temporal logics.
-
-
Verification Techniques
-
Model Checking
-
Deductive Verification: Lyapunov and Barrier Certificates
-
Simulation-Based Verification: RRTs and S-Taliro.
-
-
Application Examples
-
Real-Time Scheduling.
-
Air Traffic Management.
-
Automotive Systems.
-
Excitable Cells: Heart Tissue.
-
Anesthesia Control.
-
Insulin Infusion Control.
-
Textbook
Note that no existing textbook is going to cover everything in the syllabus. But one book comes close to covering mode than 80% in significant detail.
Main Textbook
We will be using the book
-
Principles of Cyber-Physical Systems by Rajeev Alur.
The book will be published by MIT press in December 2014. Prof. Alur has kindly allowed us the use of a draft for use in this class. We will distribute the relevant chapters as the course progresses.
For certain parts of the syllabus, we will use different books including
-
Feedback Systems: An Introduction to Scientists and Engineers by Karl Astrom and Richard Murray.
-
Introduction to Embedded Systems by Edward Lee and Sanjit Seshia (Close to Prof. Alur's book but differs in emphasis on certain topics)
-
Surveys, Papers and Lecture Notes from various authors.
Course Work
Course work will involve:
-
Weekly assignment problems given out each week.
-
Some assignments may involve the use of tools such as Matlab Simulink(tm)/Stateflow(tm) and other open source tools.
-
-
Course Project due at the end of the class. Projects may involve:
-
Modeling and Designing a nontrivial CPS using the ideas taught in the class,
-
Reading papers on a advanced topic relevant to the class, or
-
Working with a verification tool and evaluating it on a set of benchmarks.
-
Exams
There will be two in-class ''midterm'' quizzes that will test the material learned. Midterms will be announced two weeks in advance, and held in class.
Course Participation
Class participation is awarded based mainly on your class preparation, as judged by your general attendance, classroom behavior, interaction in class, willingness to answer questions in class and at the on-line forums, and demonstrating knowledge of weekly reading during problem solving time.
Grading
The final grade will be calculated by adding up grades for various parts of the class:
-
Assignments: 60%
-
Project: 30%
-
Class Participation: 10%
Collaboration Policy
The collaboration policy is rather simple:
-
Inspiration is free: you may discuss homework assignments with anyone. You are especially encouraged to discuss solutions with your instructor and your classmates.
-
Plagiarism is forbidden: the assignments that you turn in should be written entirely on your own. While writing the assignment you are not allowed to consult any source other than the textbook(s) for the class, your own class notes or the lecture notes for the class. Copying/consulting from the solution of another classmate constitutes a violation of the course's collaboration policy and the honor code.
-
Do not search for a solution on-line: You may not actively search for a solution to the problem from the internet. This includes posting to newsgroup or asking experts at other universities.
-
When in doubt, ask: If you have doubts about this policy or would like to discuss specific cases, please ask the instructor.
Honor Code
We will expect strict adherence to our our honor code. Please read and understand the code thoroughly. If in doubt, ask the instructor. At the end of the day, honor code violators hurt themselves by sacrificing their integrity and risking hard-earned reputation for a few measly grade points.
Introduction to Embedded Systems Lee Seshia Solution Manual
Source: https://home.cs.colorado.edu/~srirams/courses/csci7000-fall14/index.html
0 Response to "Introduction to Embedded Systems Lee Seshia Solution Manual"
Post a Comment