Using non failure-safe components in the implementation of safety-critical systems is desirable because of the extremely high cost of certified components. In order to enhance the safety of such systems, we adopt a solution based on the idea of verifying each single execution of the software running upon them. In particular, we consider the class of translation-based tools used in the development of safety-critical systems. In order to perform the verification in an automatic and efficient way, we follow an innovative approach, by distinguishing an off-line and an on-line verification phases. Each proof in the two phases is guaranteed correct thanks to the use of a logging-and-checking architecture for the tools used to generate them. We describe in detail the off-line and on-line logging-and-checking methodology, its application in the frame of an industrial project, and the ongoing logging-and-checking redesign of a state-of-the-art prover which we intend to use in future applications

Certification of Translators via Off-line and On-line Proof Logging and Checking

Bertoli, Piergiorgio;Cimatti, Alessandro;Giunchiglia, Fausto;Traverso, Paolo
1997

Abstract

Using non failure-safe components in the implementation of safety-critical systems is desirable because of the extremely high cost of certified components. In order to enhance the safety of such systems, we adopt a solution based on the idea of verifying each single execution of the software running upon them. In particular, we consider the class of translation-based tools used in the development of safety-critical systems. In order to perform the verification in an automatic and efficient way, we follow an innovative approach, by distinguishing an off-line and an on-line verification phases. Each proof in the two phases is guaranteed correct thanks to the use of a logging-and-checking architecture for the tools used to generate them. We describe in detail the off-line and on-line logging-and-checking methodology, its application in the frame of an industrial project, and the ongoing logging-and-checking redesign of a state-of-the-art prover which we intend to use in future applications
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/1455
 Attenzione

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

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