An R&D Centre at IIT Bombay

Sponsored Projects

Formal Verification of Flight Software:
Sponsor:Aeronautical Development Agencies, Bangalore.

The objective of the project is to validate the software modules(C code) used in this one Flight software unit using formal verification techniques. This software in the unit has a number of requirements like panel display and control, some communication protocols, input validation, computational requirements etc. A suitable part of the software has been taken up for verification. These routines are written in the language C. The project will involve the analysis and verification of these C functions.

The tool C2SPL developed in-house is extensively used in this project. Currently the formal specification of the various functions in the unit are completed and the verifcation us in progress. The verification is carried out using the tool STeP (Stanford Theorem Prover), developed at Stanford University.

Verification of Hardware controller:
Sponsor: Texas Instruments, Bangalore.

In this project, we propose to explore the possibility of formal verification of some of the hardware controller developed at Texas Instruments (India) Pvt. Ltd. The objective of the project is to apply model checking techniques to verify a medium sized industrial design. The design considered for this purpose is a hardware controller developed at TI, Bangalore. As a pilot example, the project work will start with the verification of a smaller controller. Once this is completed, verification of the main hardware controller will be undertaken.

The commercial model-checking tool, Formal-Check developed and marketed by Cadence, will be used for verification.

Currently, the verification of the pilot example is completed. A better understanding of the tool Formal-check has been acquired. The verification of main hardware controller is in progress now.