Nov-Dec 2013 EDITION Formal Verification of Software

Abstract:For the formal verification of software, a verification tool has to be selected and it should check whether the system meets the specification given by the developer. The SPIN (Simple Promela Interface) tool is selected as the verification tool. SPIN accepts two inputs, PROMELA (Process Meta Language) and LTL (Linear Temporal Logic).The code to be tested is in C language. A conversion of C code into PROMELA by preserving the logic has to be done.After the detailed study of code and with the help of specifications given by the developer, the desired states are identified and these states are manually represented in LTL formula. Desired states are those, which should be met at every part of the code. The other important task is to make SPIN tool facilitate unit testing.For this, C code has to be embedded with promela and make same variables accessed by both languages. After completion of above mentioned tasks the PROMELA and LTL are fed to SPIN, giving the outputs as reached/unreached states