Course Description:

Modern automobiles, medical devices, avionics systems, complex robots, smart energy and infrastructure systems are all examples of cyber-physical systems (CPS). Such systems are characterized by two main aspects: (1) physical components (e.g. electrical, electronic, mechanical, hydraulic mechanisms), and (2) software that is used to control the behavior of the physical components. Increasingly, such CPS applications are seeking to become autonomous with the help of artificial intelligence components trained using machine learning algorithms. In such a setting, an important question is how we reason about the correctness, safety, reliability and security of such systems. In this seminar course, we will explore the key literature in this area including the latest research results.

Learning Objectives:

  1. Gain basic familiarity with formal techniques for reasoning about correctness of CPS applications.
  2. Understand verification approaches based on automatic techniques like model checking as well as less automated deductive methods.
  3. Learn how system specifications are expressed using real-time temporal logics.
  4. Learn about requirement-based testing approaches.
  5. Learn about CPS applications that use AI-based components such as neural networks.
  6. Learn how to critically read a technical research paper in this topic.

Instructor:

Jyotirmoy (Jyo) V. Deshmukh

Lectures:

SAL 322, Tuesday 2:00 - 5:20pm

Office hours:

By Appointment.

Prerequisites:

CSCI 170, CSCI 270 (preferred)

Co-Requisites:

None.

Recommended Preparation:

Basic background in automata theory, formal languages.