System Analysis & Verification (SAVE) Lab

Applying Formal Methods to ensure Reliable Engineering Systems

Introduction

These days hardware and software systems are increasingly being used in safety-critical domains, such as electronic military and medicine equipment and automated transportation systems. This fact makes the accuracy of their analysis very important as an uncaught system bug may endanger human life or lead to a significant financial loss. Traditionally, the verification of these systems has predominantly been accomplished by computer simulation. However, it does not ascertain 100% correctness and thus has primarily been responsible for many unfortunate incidents that happened due to an erroneous hardware or software system deployed in a safety-critical domain.

The primary focus of our research is on using formal methods, which are based on mathematical techniques and thus unlike simulation ensure 100% precise results, for the analysis and verification of hardware, software, and embedded systems. In particular, we aim at using theorem proving , which is one of the widely used formal methods, to develop methodologies, algorithms and tools for the accurate analysis of systems that are continuous in nature or interact with continuous physical environments.

Besides the formal verification, we are also involved in designing hardware systems. Some of the ongoing activities in this aspect are concentrated on designing Network-on-chip (NoC) architectures, Reconfigurable architectures ,transistor-level analog circuits and tele-surgical robots .