VFRAME is one of ANSALDO`s software driven vital architectures for safety critical products. This paper describes a project whose results is the development of an `embedded verifier`, i.e. a system integrated within VFRAME and able to certify the correctness of one of VFRAME components, a compiler. The embedded verifier satisfies two precise requirements. First, the compiler must be certified in a fully automatic and efficient way. Second, the embedded verifier must be itself certified, in a way which can be easily understood and validated by end users
A Provably Correct Embedded Verifier for the Certification of Safety Critical Software
Cimatti, Alessandro;Giunchiglia, Fausto;Traverso, Paolo;
1997-01-01
Abstract
VFRAME is one of ANSALDO`s software driven vital architectures for safety critical products. This paper describes a project whose results is the development of an `embedded verifier`, i.e. a system integrated within VFRAME and able to certify the correctness of one of VFRAME components, a compiler. The embedded verifier satisfies two precise requirements. First, the compiler must be certified in a fully automatic and efficient way. Second, the embedded verifier must be itself certified, in a way which can be easily understood and validated by end usersFile 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.
