CIS 540: Principles of Embedded Computation

CIS 540: Principles of Embedded Computation, Fall 2009

Logistics

Instructor: Rajeev Alur ( alur@cis)
Lectures: Mon, Wed 10.30 -- 12.00, Towne 305
Office hour: Tues 4.30 -- 5.30, Levine 609
Teaching Assistant: Truong Nghiem ( nghiem@seas); Office Hour: Monday 2-3, Levine 558

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 CIS or CE as an upper-level elective.

Topics

Introduction to Model-based Design
- State machines
- Dynamical systems
- Timed Systems
- Hybrid Systems
- Observational Semantics and Refinement
Models of Interaction
- Asynchronous models
- Dataflow networks
- 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
- Abstractions and compositional verification
Modeling for Performance
- Probabilistic models: Markov chains, Continuous-time Markov chains, Markov decision processes
- Steady state analysis
- Modeling and analyzing quantitative properties such as power usage

Grading

There will be periodic homework assignments consisting of theoretical problems. There will be a midterm and a final exam. A significant component of the evaluation will be the class project.

Tentative Schedule

Sept 9, 14, 16, 21: Synchronous modeling
Sept 28, 30, Oct 5: Safety requirements (note: no class on Sept 23)
Oct 7, 12, 14: Asynchronous models
Oct 21, 26, 28: Model checking
Nov 2, 4, 9: Dynamical systems
Nov 11, 16, 18: Real-time systems
Nov 23, 25, 30: Hybrid systems
Dec 2, 7, 9: Real-time scheduling

Lecture Notes

This is a preliminary draft of a potential textbook on this subject. If you have any corrections or comments regarding either the exposition style or the technical topics, please email ( alur@cis).

Maintained by Rajeev Alur