GIAN Course on
Verification of Cyber Physical Systems
8-12 January 2018
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.
The venue of the workshop is Room L9, Center for Continuing Education (CCE), (Opposite Security Office, ATM Gate) IISc, Bangalore 560012.
|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.
|Mon, 8 Jan 2018||8:45am||Registration, Breakfast, and Inauguration|
|9:30am||Introduction and Motivation||Pavithra Prabhakar|
|9:30am||Hybrid Automata: Syntax and Semantics||Pavithra Prabhakar|
|2:00pm||Tutorial: Modelling hybrid systems|
|Tue, 9 Jan 2018||9:30am||LTL Specifications and Model-Checking||Deepak D'Souza|
|11:30am||CTL Specifications and Model-Checking||Deepak D'Souza|
|2:00pm||Tutorial: Model-Checking with Spin.
Traffic Light model in Spin
|Wed, 10 Jan 2018||9:30am||Dynamical systems||Pavithra Prabhakar|
|11:30am||Stability analysis||Pavithra Prabhakar|
|2:00pm||Tutorial: Sum-of-squares programming|
|Thu, 11 Jan 2018||9:30am||Bounded Verification of Hybrid Systems||Pavithra Prabhakar|
|11:30am||Bounded Error Approximations, symbolic execution||Pavithra Prabhakar|
|2:00pm||Tutorial: Bounded verification using the BEAVER tool|
|Fri, 12 Jan 2018||9:30am||Bisimulation algorithm, Predicate abstraction, and Hybridization||Pavithra Prabhakar|
|11:30am||Algorithmic verification of stability||Pavithra Prabhakar|
|2:00pm||Tutorial: Algorithmic stability analysis using AVERIST tool|
Deepak D'Souza, IISc Bangalore