CS637: Embedded and Cyber-Physical Systems

Fall 2016 (July 27, 2016 - November 11, 2016)

Lecture Hours: Monday and Thursday 12 noon to 1:30 pm
Office Hour: Friday 12 noon to 1:00 pm

Lecture Venue: KD 102

Instructor: Indranil Saha (Email: isaha[at]cse[dot]iitk[dot]ac[dot]in)
Teaching Assistants: Tanmoy Kundu (Email: tanmoy[at]cse[dot]iitk[dot]ac[dot]in)
                                    Danish Khalidi (Email: 16111013[at]iitk[dot]ac[dot]in)

Overview

A cyber-physical system is a collection of interconnected computing devices interacting with the physical world. The computing devices together constitute a cyber system that regulates the behavior of the physical world. The cyber system closely monitors the physical world through sensors, computes required control laws based on the current state of the physical world, and applies the computed control law to the physical world through actuators. The sensors, the controllers, and the actuators are developed on top of an embedded platform. Thus, the cyber component of a cyber-physical system is often termed as an embedded control system.

Developing an embedded control system requires the understanding of the physical world with which the system has to interact. The understanding of the physical world is captured in a faithful model that is used for synthesizing feedback control laws using control theoretic methods. Implementing the feedback control law on the embedded computing platform requires addressing the challenges of embedded computing, for example, the availability of limited resources in terms of computing power and memory, stringent timing requirements, and so on. Moreover, most cyber-physical systems are safety-critical. Thus, it is essential that the correctness of such systems is established through the use of formal verification techniques.

The course will cover the modeling, implementation and verification issues related to developing a cyber-physical system. Through the discussion of the implementation of an embedded control system, the course will cover the basic design principles of an embedded system.


Prerequisites

The course does not have any formal prerequisites. The students are expected to have mathematical maturity of the level of an undergraduate degree in engineering. However, some familiarity with finite state machines and ordinary differential equations, and programming experience will be helpful.


Topics

  • Modeling Dynamic Behaviors and Control: Continuous Dynamics, Feedback Control, Discrete Systems, Hybrid Systems, Composition of State Machines, Concurrent Models of Computation
  • Design and Implementation: Sensors and Actuators, Embedded Processors, Memory Architectures, Input and Output Interface, Multitasking, Scheduling
  • Analysis and Verification: Invariants and Temporal Logic, Equivalence and Refinement, Rechability Analysis, Model Checking, Timing Analysis


    • Grading Policy

    Homework Assignments - 20%
    Mid-Semester Examination - 20%
    End-Semester Examination - 30%
    Project - 30%

    Our department follows this anti-cheating policy strictly.


    Exam Schedule and Deadlines

    Homework
    Homework 1 (Deadline: August 22, 2016)
    Homework 2 (Deadline: September 7, 2016)
    Homework 3 (Deadline: September 29, 2016)
    Homework 4 (Deadline: October 16, 2016)
    Homework 5 (Deadline: November 3, 2016)

    Project
    Initial Project Proposal Submission (Deadline: September 8, 2016)
    Project Proposal Presentation (Scheduled on September 19, 2016 and September 22, 2016)
    Final Project Proposal Submission (Deadline: September 29, 2016)
    Intermediate Report Submission (Deadline: October 17, 2016)
    Final Project Presentation (Scheduled on November 3, 2016, November 7, 2016 and November 10, 2016)
    Final Report Submission (Deadline: November 14, 2016)

    Mid-Semester Examination
    September 16, 2016 (Friday) 1:00 pm to 3:00 pm at RM101

    Final Examination
    November 24, 2016 (Thursday) 4:00 pm to 7:00 pm at RM101


    Reading and Homework Assignments

    July 28, 2016:
       Read Chapter 1 of [LS15]. Read [Lee08].
       Make yourself familiar with Simulink.

    August 1, 2016:
       Read Chapter 2 of [LS15]. Read [OSS12].
       Work out Problem 7(a) in the Exercises of Chapter 2 in [LS15]. This is part of Homework Assignment 1.

    August 4, 2016:
       Read Example2.8 (vehicle steering), Section 3.1 (cruise control), Example 6.4 (feedback control for vehicle steering), Example 7.3 (observer design for vehicle steering) in reference [AM09]. Glance through Chapter 2-7 and 10.
       The states of the linearized model of the vehicle steering system represent the lateral deviation of the vehicle from the x-axis and the angle between the vehicle axis and the x-axis. The output of the linearized model is only the first state. Construct a Simulink model for the vehicle steering system with its controller that includes an observer. The dynamics are available in Example 6.4 and Example 7.3 in [AM09]. Apply a sinusoidal signal as the reference trajectory that specifies the desired deviation of the vehicle from the x-axis with time. Plot the output (lateral deviation of the vehicle from the x-axis) with time. This problem part of Homework Assignment 1. This is part of Homework Assignment 1.

    August 8, 2016:
       Read Chapter 3 of [LS15].
       Work out Problem 5(a), 5(b) and 5(c) in the Exercises of of Chapter 3 in [LS15]. This is part of Homework Assignment 1.

    August 11, 2016:
       Read Chapter 4 of [LS15]. Read Section 1, 2.1 and 2.2 of [Ras05]. Read [ASK04].
       Make yourself familiar with Simulink Stateflow.
       Work out Problem 2 and Problem 13 in the Exercises of Chapter 4 in [LS15]. This is part of Homework Assignment 1.

    August 18, 2016:
       Read Chapter 5 of [LS15]. Read [Harel87].
       Work out Problem 3 in the Exercises of Chapter 5 in [LS15]. This is part of Homework Assignment 2.
       In the hierarchical state machine in Figure 5.17 of [LS15], suppose that the transition from state B to state A is a preemptive transition. Construct an equivalent flat finite state machine giving the semantics of the hierarchical state machine. This problem is part of Homework Assignment 2.

    August 22, 2016:
       Read Chapter 6 of [LS15].
       Explore "Ports and Subsystems" and "Signal Routing" libraries in Simulink. Study the modeling of a Fault-Tolerant Fuel Control System and an Anti-Lock Braking System in Simulink Examples.
       Work out Problem 1 and Problem 8 in the Exercises of Chapter 6 in [LS15]. This is part of Homework Assignment 2.

    August 29, 2016:
       Read [SRR16] up to Section III.
       Read [Rus02] up to Section 4. You may ignore the discussion on verification.
       [KB03] is the seminal paper on Time-Triggered Architecture by Hermann Kopetz.

    September 1, 2016:
       Read Chapter 7 of [LS15].
       Those who are intereseted in Indoor Localization Techniques should read [Mau12].
       Provide the state-space representation of the dynamics of a DC Motor. Assume that there is no additional load on the motor. Next, Design a Simulink model to capture the dynamics and simulate the model for an input PWM voltage signal with magnitude 1V, frequency 1 kHz and duty cycle 0.1. Assume that the kinetic friction of the motor is negligible. Take the values of the other parameters from Example 7.13 in [LS15]. This is part of Homework Assignment 3.

    September 5, 2016:
       Read Chapter 8 of [LS15].
       Read [AMST10] to get the details on the fixed-point implementation of control software.
       Consider the vehicle steering control problem in Example 6.4. Assume that k1 = 1, k2 = 1.6 and kr = 1. Model the control system in Simulink using double precision floating point arithmetic. Now replace the model of the controller with the ones that use 16 bit and 8-bit fixed-point arithmetic. In each case, determine the fixed-point data types precisely. Plot the difference between the first state for the floating point controller and that for the fixed point controllers. Generate code for both the floating point controller and the fixed-point controllers using different optimization options. Describe your experience with code generation. This is part of Homework Assignment 3.

    September 8, 2016:
       Read Chapter 9 of [LS15].
       Work out Problem 1 in the Exercises of Chapter 9 in [LS15]. This is part of Homework Assignment 3.

    September 26, 2016:
       Read Chapter 10 of [LS15].
       Work out Problem 4 in the Exercises of Chapter 10 in [LS15]. This is part of Homework Assignment 4.

    September 29, 2016:
       Read Chapter 11 of [LS15].
       Work out Problem 2 in the Exercises of Chapter 11 in [LS15]. This is part of Homework Assignment 4.

    October 3, 2016:
       Read Chapter 12 of [LS15]. Read [LL73].
       Work out Problem 3 and Problem 6 in the Exercises of Chapter 12 in [LS15]. This is part of Homework Assignment 4.

    October 6, 2016:
       Read Chapter 13 of [LS15]. Read Section 5.1, 5.1.1, 5.1.2 and 5.1.3 from [BK08].
       Work out Problem 2 and Problem 4 in the Exercises of Chapter 13 in [LS15]. This is part of Homework Assignment 5.

    October 17, 2016:
       Read Chapter 14 of [LS15].
       Work out Problem 3 in the Exercises of Chapter 14 in [LS15]. This is part of Homework Assignment 5.

    October 20, 2016:
       Read Chapter 15 of [LS15].
       Make yourself familiar with Spin Model Checker.
       Work out Problem 1 in the Exercises of Chapter 15 in [LS15]. This is part of Homework Assignment 5.

    October 24, 2016:
       Read about CTL in Section 6.2, 6.2.1 and 6.2.2 in [BK08]. Read about Timed Automata in Section 9.1. Read about TCTL in Section 9.2 (up to page 700). The seminal paper on Timed Automata is [AD94].
       Make yourself familiar with UPPAAL Model Checker.
       Verify Fischer's Mutual Exclusion protocol using UPPAAL. The example is available with UPPAAL tool. Measure the time required to verify the protocol for increasing number of partcipants in the protocol. This is part of Homework Assignment 5.

    October 27, 2016:
       Read Chapter 16 of [LS15]. Read [WEE+08] (Consider reading up to page 19, and if possible proceed further).
       Work out Problem 2 in the Exercises of Chapter 16 in [LS15]. This is part of Homework Assignment 5.

    October 31, 2016:
       Read Chapter 17 of [LS15].    Read [CAS09].


    Lecture Schedule


    Lecture Date Topic References
    1July 28, 2016Introduction to the course[LS15 - Ch 1]
    2August 1, 2016Modeling Dynamic Behaviors - Continuous Dynamics[LS15 - Ch 2]
    3August 4, 2016Basics of Feedback Control Theory[AM09]
    4August 8, 2016Modeling Dynamic Behaviors - Discrete Dynamics[LS15 - Ch 3]
    5August 11, 2016Hybrid Systems[LS15 - Ch 4]
    --August 15, 2016 Holiday: Independence Day
    6August 18, 2016Composition of State Machines[LS15 - Ch 5]
    7August 22, 2016Concurrent Models of Computation[LS15 - Ch 6]
    --August 25, 2016 Holiday: Janmastami
    8August 29, 2016Time-Triggered Architecture[KB03]
    9Swptember 1, 2016Sensors and Actuators[LS15 - Ch 7]
    10September 5, 2016Embedded Processors[LS15 - Ch 8]
    11September 8, 2016Memory Architectures[LS15 - Ch 9]
    --September 12, 2016 Holiday: Idu'l Zuha (Bakrid)
    --September 15, 2016 Mid-Semester Examination
    --September 19, 2016Project Proposal Presentation
    --September 22, 2016Project Proposal Presentation
    12September 26, 2016Input and Output[LS15 - Ch 10]
    13September 29, 2016Multitasking[LS15 - Ch 11]
    14October 3, 2016Scheduling [LS15 - Ch 12]
    15October 6, 2016Invariants and Temporal Logic[LS15 - Ch 13]
    --October 10, 2016 Mid-Semester Recess
    --October 13, 2016 Mid-Semester Recess
    16October 17, 2016Equivalence and Refinement[LS15 - Ch 14]
    17October 20, 2016Reachability Analysis and Model Checking[LS15 - Ch 15]
    18October 24, 2016Verification of Timed Systems[BK08 - Ch 9]
    19October 27, 2016Quantitative Analysis[LS15 - Ch 16]
    20October 31, 2016Security and Privacy[LS15 - Ch 17]
    --November 3, 2016Project Presentation
    --November 7, 2016Project Presentation
    --November 10, 2016Project Presentation


    Projects

    Project Equipment
    For your project you can borrow an Intel Galileo board from the instructor.
    Here is a list of sensors and actuators available at IIT Kanpur Robotics Club. You may request the club to issue some components to you for your class project.

    Project Grading Scheme
    Your project will be graded out of 100 based on the following scheme:
    Initial Proposal - 10
    Project Proposal Presentation - 15
    Final Proposal - 10
    Intermediate Project Report - 10
    Final Project Presentation - 25
    Final Project Report - 30

    Template for Project Proposal
    The Project Proposal will be roughly of three pages containing the following information:

    Template for Project Report
    The Project Report should be roughly of six pages containing the following information: For your report, you are requested to use the following template: Latex (preferred) MS Word (preferred)

    List of Projects
    1. Panic Watch (Aakash Gupta, Prashant Kumar and Rahul Tudu)
    2. Failure Handling in Swarm of Quadrotors (Gaurav Verma, Lakshay Garg and Mayank Mittal)
    3. Home Automation System (Hemant Kumar and Ankit Kumar)
    4. Indoor Positioning and Mapping (Swati gupta, Shubh gupta and Deepak gangwar)
    5. Gesture Control of Quadcopter and Indoor Navigation (Gourav Katha, Siddharth Lal, Maniratnam Mandal and Ankit Singh)
    6. Modeling Semi-Autonomous Vehicle Driving for Indian Terrain (Utsav Gupta, Satyam Dwivedi and Avinash Chambhare)
    7. Phone Guided Robot (Sqn Ldr Sunil Sharma, Lt Cdr Amit Singh and Abhay Kumar)
    8. Obstacle Avoidance of Autonomous Robot (Saurabh Kumar and Rohit Negi)
    9. SHERLOCK: Smart Home Entry Registration and Locking System (Prawal Gangwar, Prakhar Jawre and Saksham Agarwal)
    10. BuDDy: An Autonomous Walking Assist Robot (Vemula Akhil, Aashish Kolluri and Harish Yadav)
    11. Vehicle Control Systems with Features of IoT (Sqn Ldr K Vijaya Kumar, Maj Nikhil Raj Jainvi, Lt Cdr Debjyoti Banerjee and Lt Cdr Ravi Shankar Singh)


    References

    [AD94] Rajeev Alur, David L. Dill: A Theory of Timed Automata. Theor. Comput. Sci. 126(2): 183-235 (1994).
    [AM09] K. J. Astrom and R. M. Murray. Feedback Systems: An Introduction for Scientists and Engineers. Prince- ton University Press, 2009. http://www.cds.caltech.edu/~murray/amwiki/index.php/Main_Page.
    [AMST10] A. Anta, R. Majumdar, I. Saha and P. Tabuada. Automatic Verification of Control System Implementations. EMSOFT 2010.
    [ASK04] Aditya Agrawal, Gyula Simon, Gabor Karsai. mantic Translation of Simulink/Stateflow Models to Hybrid Automata Using Graph Transformations. Electronic Notes in Theoretical Computer Science 109 (2004) 43-56.
    [BK08] C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.
    [CAS09] A Cardenas, S Amin, B Sinopoli, A Giani, A Perrig, S Sastry, Challenges for securing cyber physical systems, Workshop on future directions in cyber-physical systems security, 2009.
    [Harel87] D. Harel. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming 8 (1987) 231-274.
    [KB03] Hermann Kopetz and Gunther Bauer, The Time-Triggered Architecture, Proceedings of the IEEE 91(1): 112 - 126, 2013.
    [Lee08] Edward A. Lee. Cyber-Physical Systems: Design Challenges. IRORC 2008.
    [LS15] Edward A. Lee and Sanjit A. Seshia, Introduction to Embedded Systems, A Cyber-Physical Systems Approach, Second Edition, http://LeeSeshia.org, ISBN 978-1-312-42740-2, 2015.
    [Mau12] Rainer Mautz. Indoor Positioning Technologies. Habilitation Thesis, ETH Zurich, 2012.
    [LL73] C. L. Liu and James W. layland. Scheduling Algorithms for Multiprogramming in a Hard Real-Time Environment. Journal of the ACM, Vol. 20, No. 1, pages 46-61, 1973.
    [OSS12] Sam Owre, Indranil Saha and Natarajan Shankar. Automatic Dimensional Analysis of Cyber-Physical Systems. FM 2012.
    [Ras05] Jean-François Raskin. An Introduction to Hybrid Automata. Handbook of Networked and Embedded Control Systems, pages 491-517, 2005.
    [Rus02] John Rushby. An Overview of Formal Verification For the Time-Triggered Architecture. FTRTFT 2002.
    [SRR16] Indranil Saha, Suman Roy, S. Ramesh: Formal Verification of Fault-Tolerant Startup Algorithms for Time-Triggered Architectures: A Survey. Proceedings of the IEEE 104(5): 904-922 (2016).
    [WEE+08] Wilhelm, R., J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenstr. The worst-case execution-time problem - overview of methods and survey of tools. ACM Transactions on Embedded Computing Systems (TECS), 7(3), pages 1–53, 2008.