GIAN

GIAN Course on

Verification of Cyber Physical Systems

8-12 January 2018
Indian Institute of Science, Bangalore.

IISc

Instructors

About the course

Cyber-physical systems (CPS) are a new genre of software controlled physical systems that arise in applications involving automotive, aerospace, robotics, process control and medical devices. They integrate computation, control and communication in novel ways to provide sophisticated functionalities such as autonomous driving in self-driving cars and automated load balancing in smart grids. On one hand, CPS enable systems that guarantee enhanced safety, security and efficiency. On the other hand, they are extremely safety critical, since, software or system errors can be disastrous. The grand challenge towards the development and deployment of CPS is to develop methodology that can provide high-confidence in their correct functioning.

Formal methods is a branch of computer science that deals with rigorous methods for analysis of systems that provide provable guarantees about the correctness. A verification algorithm takes as input a mathematical model of the system and a formal unambiguous description of the correctness specification and outputs a proof of the correctness of the system in the case that the system is correct.

In this course, we will discuss state-of-the-art formal verification techniques for CPS design and analysis. In particular, we will focus on an important aspect of CPS, namely, the interaction between discrete and continuous elements that arise as a result of the interaction of software (discrete) with physical systems (continuous). We capture these behaviors in the framework of hybrid automata, and provide detailed coverage of the core algorithms and software tools that have been developed for the verification of these hybrid automata.

Venue

The venue of the workshop is Room L9, Center for Continuing Education (CCE), (Opposite Security Office, ATM Gate) IISc, Bangalore 560012.

Fees and Registration

Category Fees
Non-Indian USD 500
Indian Industry INR 15,000
Indian Academic / Government Research Lab INR 10,000
Indian Student INR 2,000

Those who would like to attend the course are requested to register themselves on the GIAN portal, and then on the course registration page.

Limited on-campus accommodation is available, and can be provided on request and payment of applicable charges.

Schedule of talks

Day Time Title Lecturer
Mon, 8 Jan 2018 8:45am Registration, Breakfast, and Inauguration
9:30am Introduction and Motivation Pavithra Prabhakar
11:00am Coffee Break
9:30am Hybrid Automata: Syntax and Semantics Pavithra Prabhakar
1:00pm Lunch
2:00pm Tutorial: Modelling hybrid systems
Tue, 9 Jan 2018 9:30am LTL Specifications and Model-Checking Deepak D'Souza
11:00am Coffee Break
11:30am CTL Specifications and Model-Checking Deepak D'Souza
1:00pm Lunch
2:00pm Tutorial: Model-Checking with Spin.
Traffic Light model in Spin
Wed, 10 Jan 2018 9:30am Dynamical systems Pavithra Prabhakar
11:00am Coffee Break
11:30am Stability analysis Pavithra Prabhakar
1:00pm Lunch
2:00pm Tutorial: Sum-of-squares programming
Thu, 11 Jan 2018 9:30am Bounded Verification of Hybrid Systems Pavithra Prabhakar
11:00am Coffee Break
11:30am Bounded Error Approximations, symbolic execution Pavithra Prabhakar
1:00pm Lunch
2:00pm Tutorial: Bounded verification using the BEAVER tool
Fri, 12 Jan 2018 9:30am Bisimulation algorithm, Predicate abstraction, and Hybridization Pavithra Prabhakar
11:00am Coffee Break
11:30am Algorithmic verification of stability Pavithra Prabhakar
1:00pm Lunch
2:00pm Tutorial: Algorithmic stability analysis using AVERIST tool

Organization

Deepak D'Souza, IISc Bangalore
Email: deepakd@iisc.ac.in
Phone: 91-80-22932368