- Instructor: Rajeev Alur ( alur@cis)
- Lectures: Monday, Wednesday, 10.30 -- Noon, Moore 212
- Recitation: Friday, Noon -- 1pm, Moore 212
- Teaching Assistant: Rahul Vasist ( rahulr@seas)
- Office Hours: Rajeev Alur: Tuesday, 4-5pm (Levine 609); Rahul Vasist: Monday, 4-5pm (Education Commons, Room 230)

Draft is available to registered students: stop by at the copy center (ground floor of Levine), and ask for a copy. Comments on the textbook draft are most welcome (typos, errors, suggestions for improving the explanation/presentation). Email your comments to alur@cis.

- Six Homeworks (30%): Each such homework will consist of theoretical problems.
- Three Modeling Projects (15%): Each such project will involve modeling and analysis. First project involves the model checker SPIN, the second involves Matlab, and the third will use Stateflow/Simulink.
- Midterm (20%): In-class exam (March 5)
- Final Exam (35%) (May 9)

- Introduction: Jan 15 Slides
- Chapter 2: Synchronous Models; Jan 24 Slides, Jan 27 Slides, Jan 29 Slides, Feb 3 Slides
- Chapter 3: Safety Requirements; Feb 5 Slides, Feb 10 Slides, Feb 12 Slides, Feb 17 Slides
- Chapter 4: Asynchronous Models; Feb 19 Slides, Feb 24 Slides, Feb 26 Slides, March 3 Slides
- Midterm: March 5
- Chapter 5: Model Checking; March 17 Slides, March 19 Slides, March 24 Slides, March 26 Slides
- Chapter 6: Dynamical Systems; March 31 Slides, April 2 Slides, April 7 Slides, April 9 Slides
- Chapter 7: Timed Models; April 14 Slides, April 16 Slides, April 21 Slides
- Chapter 9: Hybrid Systems; April 28 Slides, April 30 Slides
- Final Exam: Friday, May 9, 12-2, Moore 216.

- Homework 1 (Due Feb 5): Ex 2.10 (4pts); Ex 2.12 (4pts); Ex 2.16 (4pts); Ex 2.20 (8pts); Solutions
- Homework 2 (Due Feb 19); Solutions
- Homework 3 (Due Tuesday, March 4, Noon): Exercises 4.2, 4.9, 4.12, and 4.17. (5pts each); Solutions
- Preparing for the midterm
- Midterm; Solutions
- Homework 4 (Due March 28); Template SPIN code; Slides from recitation; Railroad controller example in Promela
- Homework 5 (Due April 2): Exercises 5.4, 5.5, 5.11, and 5.14. (5pts each); Solutions
- Homework 6 (Due April 18)
- Homework 7 (Due April 25): Exercises 6.14, 6.18, 7.2, and 7.8. (5pts each); Solutions
- Homework 8 (Due May 2): Exercises 7.15, 7.16, 9.2, and 9.4. (5pts each); Solutions
- Preparing for the final exam

See also the course **Foundations of cyber-physical systems** by Andre Platzer and corresponding lecture notes.

Following books are also relevant for supplementary reading for different chapters:

- Hard Real-time Computing Systems: Predictable scheduling algorithms and applications by G.C. Buttazo, Kluwer Academic Publishers, 1997.
- Model checking by Clarke, Grumberg, Peled
- Structure and Interpretation of Signals and Systems by Lee and Varaiya
- Distributed algorithms by Lynch
- A Linear Systems Primer by Antsaklis and Michel
- Introduction to Discrete-Event Systems by Cassandras and Lafortune
- Verification and Control of Hybrid Systems: A symbolic approach by Tabuada

- SPIN Model checker
- Ptolemy Project at UC Berkeley
- NuSMV Model checker
- Stateflow/Simulink by Mathworks

- 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. Finally, if you do not want to pay attention during lectures, stay home! You are not allowed to use electronic devices such as laptops and mobile phones during a lecture.
- Recitation: Recitation will not cover new material, and will be used to solve exercises, answer questions, and review background material.
- Grades will posted on canvas.
- 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