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-01-01
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 applicationsI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
