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 critical
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/1844
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact