Information Technology Reference
In-Depth Information
5
Results of Deductive Verification
Deductive verification, i.e.
unit proving
, was performed using the Frama-C
release Boron[7] and the software verification platform Why 2.26 including
Jessie. The tools were executed on Mac OS X (10.5 Leopard). The following
five automated theorem provers were referenced in our experiments:
Alt-Ergo[8], CVC3[9], Simplify[10], Yices[11], and Z3[12]. Table 1 depicts the
results obtained by deductive verification of the specified C-functions using
Frama-C and Jessie.
Automated Theorem Provers
Proof Obligations Alt-Ergo CVC3 Simplify Yices Z3
Total
74
74
74
74 74
Valid
74
72
74
70 74
Timeout
0
2
0
4
0
Proven
Yes
No
Yes
No Yes
Tabl e 1 . Results of Deductive Verification
Table 1 shows 74 verification conditions (VC), a.k.a., proof obligations,
generated by the verification condition generator, which is called implicitly
upon invoking Jessie. In our case study the three provers Alt-Ergo, Simplify
and Z3 were able to discharge all verification conditions as valid and thus
could prove that the implementation of the functions satisfies their specifica-
tion. CVC3 and Yices, on the other hand, were not able to prove all conditions
in the allocated time frame of 10 seconds and thus reported timeouts.
6
Conclusions and Future Work
We have demonstrated an approach and a procedure for verifying safety criti-
cal software components in an automated way. In our experience, an ACSL
specification can form a crucial artifact for communicating within the devel-
opment process because many participants in this process can relate to ACSL,
e.g., requirements engineers, architects, software developers or assessors.
Regarding the scalability of our approach, we think that the main focus
of deductive verification will be on relatively small, well understood software
components and on software subsystems that consist of such components.
However, even so the return on investment of deductive verification compared
to traditional component testing is not yet well understood and will be part
of our future research.
Nevertheless, there are still challenges to manage. First of all, formal
specification and deductive verification need to be properly integrated in the
software development process. This is of utmost importance for high-integrity
