A case study on model checking and deductive verification techniques of safety-critical software

Due to the growing importance of the role that software plays in critical systems, software verification process is required to be rigorous and reliable. It is well-known that test activities cannot detect all the defects in safety-critical real time software systems. One way of complementing the test activities is through formal verification. Two useful formal verification techniques are deductive verification and model checking, which allow programs to be statically checked for defects. This paper explores both techniques, by employing the CBMC and Jessie/Frama-C tools in the context of a safety-critical real time software system.This work is funded by ERDF - European Regional Development Fund through the COMPETE Programme (operational programme for competitiveness) and by National Funds through the FCT - Fundação para a Ciência e a Tecnologia (Portuguese Foundation for Science and Technology) within project FCOMP-01-0124-FEDER-020486