FORMAL VERIFICATION OF SOFTWARE IMPORTANT TO SAFETY USING THE FRAMA-C TOOL SUITE

摘要

The context of this paper is an ongoing research project. The aim is to evaluate the use of the Frama-C software analysis tool-suite to address the formal demonstration of three classes of properties in real-life software important to safety. This paper mainly discusses intrinsic properties, namely the freedom from intrinsic faults. Firstly, we show that the coverage with Frama-C of classes of software faults that might be postulated in safety or safety related control systems is satisfactory in the perspective of our application domain. The paper then presents several aspects of the experimentation performed: improvements in Frama-C, changes made to the source code for the purpose of static analysis, issues related to the memory model, and finally results obtained. It appeared in our experimentation that Frama-C can precisely represent each of the programming constructs known to cause difficulties in static analysis. Crucially, the level of precision demanded to the analysis can be adjusted by the user, depending on portions of code. Furthermore, the selectivity and absolute number of alarms obtained can be, to the best of our knowledge, compared advantageously to the state of the art in static analysis. A full analysis takes a few hours, which we consider acceptable for the purpose of independent formal verification. We also discuss ongoing work, in which we are investigating the use of Frama-C to formally verify structural properties.