CIS 540: Principles of Embedded Computation, Spring 2013
Logistics
- Instructor: Rajeev Alur
(
alur@cis)
- Lectures: Monday, Wednesday, 10.30 -- Noon, Moore 212
- Recitation: Friday, Noon -- 1pm, Moore 212
- Teaching Assistant: Zhihao Jiang (
zhihaoj@seas)
- Office Hours: Rajeev Alur: Tuesday, 4-5pm (Levine 609); Zhihao Jiang: Monday 4-5pm (??)
Introduction
This course is focused on principles underlying design and analysis of
computational elements that interact with the physical environment.
Increasingly, such embedded computers are everywhere, from
smart cameras to medical devices to automobiles.
While the classical
theory of computation focuses on the function that a program computes,
to understand embedded computation, we need to focus on the
reactive nature of the interaction of a component with its
environement via inputs and outputs, the continuous dynamics of the physical
world, different ways of communication among components, and
requirements concerning safety, timeliness, stability, and performance.
Developing tools for approaching design, analysis, and implementation of
embedded systems in a principled manner is an active research area.
This course will attempt to give students a coherent introduction to
this emerging area.
Prerequisites
This course assumes mathematical maturity, commensurate with
either ESE 210 (Introduction to Dynamical Systems), or
CIS 262 (Introduction to Theory of Computation).
It is suitable for students who have undergraduate degree in computer science,
or computer engineering, or electrical engineering. It is also suitable for
Penn undergraduates in CSCI and CMPE as an upper-level elective.
Topics
- Introduction to Model-based Design
- State machines
- Dynamical systems
- Timed Systems
- Hybrid Systems
- Models of Interaction
- Asynchronous models
- Synchronous modeling languages
- Time-triggered vs. event-triggered communication
- Interfaces and Component-based Design
-
Specification and Verification
- Requirements: Safety, Timely response, Liveness, Stability
- Temporal logics
- Analysis techniques: Simulation, Testing, Formal verification, and
Monitoring
- Basics of deductive verification: Invariants, Ranking functions
- Model checking
- Symbolic simulation
Grading
- Four Homeworks (20%): Each such homework will consist of theoretical problems.
- Two Modeling Projects (20%): Each such project will involve modeling and analysis of a toy embedded system.
First project involves the model checker SPIN, and the second involves Matlab
- Midterm (25%): In-class exam (Feb 27)
- Final Exam (35%)
Schedule and Course Notes
- Chapter 1: Synchronous Models; Jan 9, 14, 16, 23, 28
- Homework 1, Solutions
- Chapter 2: Safety Requirements; Jan 30, Feb 4, 6, 11, 13
- Homework 2, Solutions
- Chapter 3: Asynchronous Models; Feb 18, 20, 25, 27
- Homework 3; Template SPIN input; Due March 11
- Midterm (Chapters 1--3); March 13; Preparing for the Midterm
- Chapter 4: Model Checking; March 11, 18, 20
- Homework 4, Solutions
- Chapter 5: Dynamical Systems; March 25, 27, April 1
- Homework 5, Due April 8
- Chapter 6: Timed Models; April 3, 8, 10
- Homework 6, Solutions
- Chapter 7: Real-time Scheduling; April 15, 17, 22
- Final Exam (Chapters 1--7): Tuesday, May 7, 12 -- 2pm, Towne 311; Preparing for the Final
Comments on the textbook draft are most welcome (typos, errors, suggestions for improving the explanation/presentation). Email your comments to alur@cis.
Relevant Textbooks
The closest match is
Introduction to Embedded Systems -- A Cyber-Physical Systems Approach
by E.A. Lee and S.A. Seshia. (see online version)
Our course/notes cover fewer topics in greater theoretical depth.
Following books are also relevant for supplementary reading for different chapters:
Relevant Modeling and Analysis Software
Notes
- Recitation: Recitation will not cover new material, and will be used
to solve exercises, answer questions, and review background material.
- Homeworks can be submitted using Blackboard. Grades will posted on Blackboard.
- Plagiarism policy: For homeworks, projects, and exams, you can use your
personal class notes, lecture notes, and reference books.
Do not copy material from friends or from the web.
For violations of this rule, you will be reported to the Office of the Student Conduct at Penn, which may result in expulsion.
Please take the plagiarism rules serioiusly.
Start working on the homeworks and projects early, and if you get stuck, contact the instructor or the TA.
Maintained by Rajeev Alur