VFRAME is one of ANSALDO's software driven vital architectures for safety critical products. This paper describes a project whose result 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
Giunchiglia, Fausto;
1997-01-01
Abstract
VFRAME is one of ANSALDO's software driven vital architectures for safety critical products. This paper describes a project whose result 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.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
