Safety-critical systems are often designed using development support tools which perform translations of high-level specifications into lower-level counterparts. The correctness of the translation is critical to the safety of the resulting systems. However, using non failure-safe components to implement translators is desirable because of the extremely high cost of certified components. In order to ensure the correct behavior of development tools, we adopt a solution based on the idea of verifying each of their executions. 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 by designing the certifying tools according to a logging--and-checking architecture. We describe 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

A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools

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

Abstract

Safety-critical systems are often designed using development support tools which perform translations of high-level specifications into lower-level counterparts. The correctness of the translation is critical to the safety of the resulting systems. However, using non failure-safe components to implement translators is desirable because of the extremely high cost of certified components. In order to ensure the correct behavior of development tools, we adopt a solution based on the idea of verifying each of their executions. 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 by designing the certifying tools according to a logging--and-checking architecture. We describe 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
9783540651109
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: http://hdl.handle.net/11582/1730
 Attenzione

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

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