In this paper we describe an industrial project whose goal was the certification of the translator part of a tool used to develop safety critical applications. We have successfully applied a novel formal verification technique. We have constructed an `Embedded Verifier` which, for each run of the translator, verifies formally the correctness of the result of each translation, rather than the correctness of the translation algorithm or code. We call this approach `Run-time Result Formal Verification`. In order to satisfy efficiency requirements on the `Embedded Verifier`, we have decomposed the proof of correctness into two parts. The task of the `Embedded Verifier` is to prove some simple conditions at each run (on-line proof), that have been proved once for all to guarantee the correctness of the translation (off-line proof). We have addressed the problem of the correctness of the implementation of the `Embedded Verifier` itself by decomposing it into two independent programs, such that only a small kernel of the verifier is critical
Run-Time Result Formal Verification of Safety Critical Software: an Industrial Case Study
Cimatti, Alessandro;Giunchiglia, Fausto;Traverso, Paolo;Villafiorita Monteleone, Adolfo
1999-01-01
Abstract
In this paper we describe an industrial project whose goal was the certification of the translator part of a tool used to develop safety critical applications. We have successfully applied a novel formal verification technique. We have constructed an `Embedded Verifier` which, for each run of the translator, verifies formally the correctness of the result of each translation, rather than the correctness of the translation algorithm or code. We call this approach `Run-time Result Formal Verification`. In order to satisfy efficiency requirements on the `Embedded Verifier`, we have decomposed the proof of correctness into two parts. The task of the `Embedded Verifier` is to prove some simple conditions at each run (on-line proof), that have been proved once for all to guarantee the correctness of the translation (off-line proof). We have addressed the problem of the correctness of the implementation of the `Embedded Verifier` itself by decomposing it into two independent programs, such that only a small kernel of the verifier is criticalI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
