The correct, fault-free operation of safety critical systems like launch vehicles and satellites is of utmost importance. Equally important is the validation and verification of the hardware and software in these systems to avoid unexpected faults during flight. Traditional techniques like manual testing, reviews, code inspection and simulation are error prone, time-consuming and inadequate for such complex, real-time software. Here, formal verification, which involves rigorously exploring the correctness of system designs expressed as mathematical models, assumes significance.

In this talk, validation of the embedded software in the onboard computer of a launch vehicle, along with the MIL-STD-1553B communication system, through software model checking, a formal verification technique is presented. The onboard software is partly in Assembly and partly in high level language Ada. A portion of the scheduler in assembly and the fuel tank pressure vent software in Ada are modelled and verified using the model checker SPIN. The specifications to be satisfied, derived from the functional requirements, are represented as assertions/ Linear Temporal Logic formulae and included in the model. A systematic procedure for translation of Ada source code to Promela, the input language for SPIN, several possible abstractions during modelling and a procedure for definition and simulation of random errors are defined. On verification, it is found that the assertions are violated in a few instances, indicating bugs in the code. It is thus demonstrated using a case study from a real project in the aerospace field that formal verification can effectively complement existing testing methods.


All are cordially invited.