Scope and Objectives

Our aim is to grow a national knowledge centre for formal methods, targeting recent applications and safety standards in various ICT domains such as aeronautics, automotive, power, nuclear, railway, and space. Objectives include research and development of specific tools and tool repositories, industrial partnership and manpower training. We propose research centric work packages for developing tools for formal validation of control systems, networked systems, and hardware/software systems. We propose knowledge centric work packages on interpretation of safety standards, processes, and tool flows. We propose training centric work packages for developing the ecosystem for safety validation and certification procedures.

Deliverables

Final deliverables include novel tools for the problems outlined under the research centric work packages. Specifically:WP -R-1 (Deliverable from IIT Kharagpur): Tool for modelling and validation of hybrid dynamical systems consisting of software, platform and plant, using satisfiability modulo theory. WP-R-2 (Deliverable from IIT Bombay): Parallelized tools and techniques for checking formal properties of large software and hardware systems. WP-R-3 (Deliverable from IIT Kanpur): Formal tools and methodologies for verifying implementations of parts of TCP/IP protocol stack, as well as security protocol libraries such as OpenSSL, OpenSSH including TLS Library. Reverse engineering methodologies and tools proven on application layer protocols used in SCADA systems.Outcomes from the knowledge centric packages, WP-K-1 and WP-K-2, includes reports interpreting the formal verification mandate in industrial safety standards targeting specific application domains (of interest to our partners in avionics, automotive and railways), and prescribed tool flows for carrying out the recommendations.

Videos

Scientific Output

IITKGP: We have built a prototype tool framework, which takes plant dynamics and controller software as inputs. Our tool framework encodes the closed-loop execution of the plant and the controller into SMT clauses and verifies stability and other control performance properties. We have come up with a first-cut implementation of the tool. This first cut implementation helps us in identifying scalability issues with Hybrid SMT formulations. Initial results for various case studies have been reported. We have resolved certain scalability issues partially, i.e., pruning of the state-space by suitable compiler methods have been implemented. We are now working on algorithm development for adaptive step-size selection that facilitates scalable SMT techniques for Nonlinear systems. IITK: Security vulnerability study of SCADA protocols and discovery of threats in existing protocols, Formal modelling of SSL/TLS, OpenSSL vulnerability study. Methodology for translation of a nonlinear Simulink/Stateflow model to Linear Hybrid Automata (LHA) has been developed and applied to three benchmark examples manually. We are working on automating the translation process, identifying interesting properties for the example systems and verifying the generated LHA against those properties. IITB: We have already built two prototype implementations for automatic disjunctive decompositions, one of which exploits parallel computational resources, while the other exploits structure in the representation of the transition relation. These also serve as Boolean functional synthesis tools, and are among the best performing tools available today. We are also in an advanced stage of development of the ALaRE framework for specifying hybrid reachability algorithms. Finally, we have implemented some new abstract domains for our static assertion checker, and have implemented a prototype algorithm for refining the abstraction in one domain using information from another domain, without using the expensive reduced product operation. Our static analysis tool, CAnalyzer/C-SAFE, is being augmented with these new capabilities.