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||9:30am||Introduction to Hybrid Automata: Syntax, Semantics, Examples||Pavithra Prabhakar|
|11:30am||Specifications: Linear Temporal Logics, Metric Temporal Logics; Satisfiability||Pavithra Prabhakar|
|2:00pm||Tutorial: Modeling and Simulation of Hybrid Automata, Specification writing.|
|Tue, 9 Jan 2018||9:30am||Finite state automata, invariant/safety verification||Deepak D'Souza|
|11:30am||Model-checking LTL/CTL||Deepak D'Souza|
|2:00pm||Tutorial: Model-Checking with SPIN|
|Wed, 10 Jan 2018||9:30am||Continuous dynamical systems, solutions||Pavithra Prabhakar|
|11:30am||Stability analysis, eigen value and Lyapunov function based analysis||Pavithra Prabhakar|
|2:00pm||Tutorial: Template based Lyapunov function search in SOSTOOLS|
|Thu, 11 Jan 2018||9:30am||Symbolic state-space exploration, Flowpipe construction, Data structures such as Zonotopes||Pavithra Prabhakar|
|11:30am||Bounded Safety Verification using SMT solvers, Bounded Error Approximations||Pavithra Prabhakar|
|2:00pm||Tutorial: Using the BEAVER tool, bounded safety verification of robot navigation|
|Fri, 12 Jan 2018||9:30am||Safety Verification: Predicate abstraction, Abstractions of dynamics using Hybridization, and CEGAR||Pavithra Prabhakar|
|11:30am||Stability Verification: Predicate Abstraction, Hybridization and CEGAR for stability||Pavithra Prabhakar|
|2:00pm||Tutorial: AVERIST tool illustrating predicate abstraction, hybridization and CEGAR|
Deepak D'Souza, IISc Bangalore