Cyber-Physical Systems: Modeling, Verification and Synthesis

This web page discusses the general scope and policies of the graduate level course titled: "Cyber-Physical Systems: Modeling, Verification and Synthesis". For detailed schedule, coursework, and specific topics, you will have to visit the respective course web-page (see "Current and prior course offerings") for the term you are interested in.

CPS Course Scope and Motivation

Consider the future smart transportation network. Multiple autonomous vehicles will be communicating over the cloud exchanging vital information on their position, traffic and the state of the roads. Based on this information, each autonomous vehicle will be making decisions on its next action potentially at speeds exceeding 200 mph. On top of that, each vehicle is a system of systems on its own. For example, a vehicle with a hybrid powertrain will have to decide when it is appropriate to use the battery or the gas engine based on complex algorithms. This is a system of systems where cyber components interact with physical components at multiple (both architectural and time) scales. How do we go about designing such a system of systems? What are the properties of such a system of systems and what guarantees can be provided?

As another example, think of the modern close-loop medical devices. Such devices collect physiological measurements from the patient, compute the appropriate medical action and, then, apply it. How do we personalize such devices and how can we guarantee their safety?

Both examples fall under the broader category of Cyber-Physical Systems (CPS), namely, "engineered systems that are built from and depend upon the synergy of computational and physical components" (quote from the NSF CPS program). Perhaps not surprisingly, a multitude of CPS applications can be modeled using the same mathematical formalism. Thus, the theoretical foundations for modeling, analysis and synthesis of such systems are common for a large range of applications. On the other hand, specializations to particular applications can better translate theory into practical and usable software tools.

This graduate seminar-level course provides an introduction to the mathematical formalisms and resulting software tools that will help you model, analyze and synthesize CPS. In addition, selected topics from the CPSWeek conference will be covered as well. In particular, we will study:
  1. Models of software/hardware: How do we mathematically model computation for real time embedded systems? How do we model concurrent/parallel systems? What are the differences between synchronous and asynchronous computation?  
  2. Models of cyber-physical systems: How do we model physical systems? How do we model cyber and physical system behavior in a common framework? What are the properties of interest for CPS and how can we specify them?
  3. Analysis and Verification: How do we analyze and verify functional properties of CPS? How do we even state requirements? What are the challenges in verifying concurrent CPS? What are the limitations of complete verification? When automated testing can be applied?
  4. Synthesis and Control: Is automated synthesis possible? What are the limitations and challenges in controlling CPS?
  5. Selected topics if time permits:
    • Automotive systems
    • Medical devices
    • CPS with learning components in the loop
    • Security issues in CPS

The course emphasizes rigorous thinking and mathematical analysis. To connect theory to practice, we will also use current industrial strength tools based on the Matlab and Simulink platforms. 


The course has two main goals:

  1. Teach the basic theoretical foundations so that
    • you can understand the limitations and advantages of the existing theory 
    • you can use both research and industrial software tools
    • you can read the current literature from the CPSWeek conference
  2. Teach the basic skills in discovering problems that you would like to work on and, then, presenting and writing research papers  

What this course is not about: This course does not cover programming of embedded systems, distributed systems or real time systems. The course does not cover security issues of software, internet or internet of things. The course will only partially touch upon some topics that relate to feedback (networked) control, machine learning and artificial intelligence. Actually, ASU offers a variety of courses that cover all the aforementioned topics in detail and you are advised to take these courses as well.


Prerequisites


Undergraduate courses in calculus and linear algebra are mandatory. An undergraduate course in differential equations is preferred. Some knowledge about linear systems and automata theory is an advantage. However, the course will provide a short review on the necessary background material. Finally, it is assumed that the students are familiar with MATLAB (or that they are willing to pick it up on their own). Knowledge of C/C++ or Python could be needed for self defined projects.


Before registering for the course please make sure that at minimum you feel comfortable with the level of mathematical presentation in "Introduction to embedded systems" by Lee & Seshia

Current and prior course offerings

Textbooks & Readings

Note that no existing textbook is going to cover everything in the syllabus. This is a list of textbooks which may be used in the course. The list in maintained and provided as a general reference. Each term a different textbook or no textbook at all may be used.

Selected paper readings will be provided from conferences such as:

  1. CPSWeek (http://www.cpsweek.org/) and in particular the ICCPS and HSCC conferences.
  2. ESWeek (http://www.esweek.org/) and in particular the EMSOFT conference.
  3. Formal methods conferences, e.g., CAV (http://i-cav.org/) and RV (http://www.runtime-verification.org/)
  4. Robotics conferences, e.g., ICRA (https://www.ieee-ras.org/conferences-workshops/fully-sponsored/icra)

Class evaluations and feedback

I take very seriously class evaluations and feedback. During the semester, I will be posting surveys on Canvas for feedback on both the course organization and the course content. I will appreciate it if you respond to these surveys. Ideally, the changes I implement will help you better succeed in the course. Responding to surveys counts toward to your class participation grade.

Finally, it is extremely important that you respond in the final anonymous survey solicited by the university at the end of the school year. The overall feedback helps me make changes for the next year.

Classroom Behavior

Cellphones, tablets and laptops are allowed in the class for enhanced classroom experience. However, all electronic devices must be muted during class to avoid causing distractions. In addition, if you have to arrive late or leave early from the class, then please make sure that you do not cause any distractions: Do not use the door near the instructor and choose a seat as close as possible to the door.

The use of recording devices is not permitted during class. You may take pictures of the white/blackboard or the projector screen if you wish. 

Standard disclaimer: Any violent or threatening conduct by an ASU student in this class will be reported to the ASU Police Department and the Office of the Dean of Students.  

Academic Integrity

All students in this class are subject to ASU’s Academic Integrity Policy (http://provost.asu.edu/academicintegrity) and should acquaint themselves with its content and requirements, including a strict prohibition against plagiarism. All violations will be reported to the Dean’s office, who maintain records of all offenses. Students are expected to abide by the FSE Honor Code (http://engineering.asu.edu/integrity/).  


All your work for this course must be the result of your own individual effort or - when permitted - the result of your group. Having said that, you are allowed to discuss problems with your classmates or me, but you must not blatantly copy others' solutions. 


Copying (or slightly changing) solutions from online sources, other books or your classmates is easily detectable and not permitted. If such copying is detected, then a zero grade is applied to the respective assignment, a 6% penalty to the final grade for each violation, and a formal report will be filed! 


Do not forget that if you can find an answer online, then so can we! Use on-line sources for the homework and project only when explicitly allowed.

Attendance Policy & Makeup Exam Policy

I do not have an attendance policy. Come to class only if you like. Most of the material are available (or will be available) on-line. In theory, we only have to see each other during the final presentation or exam.

However, if you skip classes, you do miss the chance for class-participation bonus.

In case there is an exam or any other required class activity, e.g., poster presentation: If you cannot come to class at the scheduled day/time, then I will need some back-up documentation from a third party, e.g., a doctor, to schedule a make-up exam. Accommodations will be made for religious observances provided that students notify me at the beginning of the semester concerning those dates. Students who expect to miss class due to officially university-sanctioned activities should inform me early in the semester.  Alternative arrangements will generally be made for any examinations and other graded in-class work affected by such absences, or other medical or personal emergency reasons. 

The preceding policies are based on ACD 304–04, “Accommodation for Religious Practices” and ACD 304–02, “Missed Classes Due to University-Sanctioned Activities.”

Grade Appeal Policy 

Any regrading appeal request must be initiated within 10 business days of receiving back your graded work by sending an email to the instructor (and cc'ing the TA if applicable). We will not entertain any appeal right before, during or right after the class time since appeals are a time consuming process. 

General guidelines:

  1. If you need to understand the technical reasons on why points were reduced on homework problems, then please see the TA first. If you are not satisfied with the answer, then make an appointment with the instructor.  
  2. If you need to understand the technical reasons on why points were reduced on exams, then you may visit the instructor first. 
  3. For all other issues, please contact the instructor first.

Grievances 

If any issues arise with the course during the semester, then please follow these steps:

  1. See the instructor during office hours or by making an appointment
  2. If not satisfied with the proposed solution, then please make an appointment with the advising office
  3. If not satisfied with the proposed solution, then make an appointment with the CIDSE director

Disability Accommodations

Suitable accommodations will be made for students having disabilities. Students should notify the instructor as early as possible if they will require same. The students must be registered with the Disability Resource Center and provide documentation to that effect. 

For further information, please visit the website of the ASU Disability Resource Center at

https://eoss.asu.edu/drc/

Sexual Discrimination

Title IX is a federal law that provides that no person be excluded on the basis of sex from participation in, be denied benefits of, or be subjected to discrimination under any education program or activity.  Both Title IX and university policy make clear that sexual violence and harassment based on sex is prohibited.  An individual who believes they have been subjected to sexual violence or harassed on the basis of sex can seek support, including counseling and academic support, from the university.  If you or someone you know has been harassed on the basis of sex or sexually assaulted, you can find information and resources at 

https://sexualviolenceprevention.asu.edu/faqs

As a mandated reporter, I am obligated to report any information I become aware of regarding alleged acts of sexual discrimination, including sexual violence and dating violence. ASU Counseling Services, 

https://eoss.asu.edu/counseling

is available if you wish discuss any concerns confidentially and privately.

Copyright

All contents of these lectures, including written materials distributed to the class, are under copyright protection. Notes based on these materials may not be sold or commercialized without the express permission of the instructor. You may want to review ACD 304-06.