CIS 540: Principles of Embedded Computation
CIS 540: Principles of Embedded Computation, Spring 2016
- Instructor: Rajeev Alur
- Lectures: Monday, Wednesday, 10.30 -- Noon, Moore 212
- Recitation: Friday, Noon -- 1pm, Moore 212
- Teaching Assistant: Kuk Jang (jangkj@seas)
- Office Hours: Rajeev Alur: Tuesday, 4.30-5.30pm (Levine 609); Kuk Jang (to be announced)
This course is focused on the 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.
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.
Principles of Cyber-Physical Systems; R. Alur, 2015, MIT Press.
- Six Homeworks (30%): Each such homework will consist of theoretical problems.
- Course Project (20%): The project will focus on design, modeling, and formal analysis of
a representative cyber-physical system.
- Midterm (20%): In-class exam (March 2) Preparing for the midterm
- Final Exam (30%) (Monday, May 2, Noon -- 2pm) Preparing for the final
- Introduction: Jan 13 (Slides)
- Chapter 2: Synchronous Model: Jan 20 (Slides), 25 (Slides), 27 (Slides), and Feb 1 (Slides)
- Chapter 3: Safety Requirements: Feb 3 (Slides), 8 (Slides), 10 (Slides), 15 (Slides)
- Chapter 4: Asynchronous Model: Feb 17 (Slides), 22 (Slides), 24 (Slides), and 29 (Slides)
- Chapter 5: Liveness Requirements: March 14 (Slides), 16 (Slides), 21 (Slides), and 23 (Slides)
- Chapter 6: Dynamical Systems: March 28 (Slides), 30 (Slides), April 4 (Slides), and 6 (Slides)
- Chapter 7: Timed Model: April 18 (Slides), 20 (Slides), and 25 (Slides)
- Review: April 27
- Homework 1 (25pts): Problems 2.3, 2.14, 2.16, 2.19, and 2.23; Due Feb 8
- Homework 2, Due Feb 22
- Homework 3, Due Feb 29
- Homework 4, Due March 28.
SPIN model checker; Promela skeleton code for homework,
Promela code for railroad controller
- Homework 5 (25pts): Problems 5.4, 5.6, 5.9, 5.10, and 5.15; Due April 4
- Course project, Due April 27
- Homework 6 (25pts): Problems 6.5, 6.7, 6.13, and 6.18; Due April 18
- Lecture participation: If you are lost during a lecture, do not hesitate to ask questions.
When I ask a question, don't be shy, and answer it the best way you can.
You are not allowed to use electronic devices such as laptops
and mobile phones during a lecture except to access lecture slides.
- Recitation: Recitation will not cover new material, and will be used
to solve exercises, answer questions, and review background material.
- Grades will be posted canvas.
- We will use Piazza as a forum for course-related discussion.
- 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,
or post a question on Piazza.
Maintained by Rajeev Alur