| PhD Seminar

Name of the Speaker: Ms.Ranjani K (EE13D206)
Guide: Prof. Nitin Chandrachoodan R
Co-Guide: Prof. Kamakoti V
Online meeting link: https://meet.google.com/wvn-bftt-cms
Date/Time: 29th November 2023 (Wednesday), 2:30 PM
Title: Formal Verification Approaches for Components of Launch Vehicle Software

Abstract

The software in safety critical systems like manned space launch vehicles has been growing exponentially in terms of computations and complexity. Verification of the real-time, embedded software in these systems is thus as significant as the design. The traditional testing and simulation techniques are incomplete, time-consuming and inadequate. Therefore, approaches based on formal methods, which involve rigorously exploring the correctness of system designs expressed as mathematical models, are necessary.

In this talk, the application of software model checking and static analysis based on bounded model checking in the verification of safety critical software is explored. A custom tool chain based on bounded model checking named LLVM BMC is developed, for high level language Ada. The embedded software in the onboard computer of an aerospace system is chosen as the primary case study. A systematic procedure for model checking with SPIN tool is defined and a new verification framework for formal static analysis of Ada programs is developed. The two approaches are applied to an actual case study through accurate modelling of the execution environment for the concurrent onboard software in a launch vehicle. The results are compared and the advantages and drawbacks of both approaches are summarized. Software components in different launch vehicle missions, with bugs found during various stages in development - testing, code inspection, simulations and launch are fed to the tool. It is seen that violations of the stated properties are detected by LLVM BMC, thus demonstrating the effectiveness of formal verification in real-world scenarios.