There is now a way to mathematically prove that the software governing critical safety and security systems in aircraft and motor vehicles is free of a large class of errors – long before the plane takes off or the car's engine starts.
The Secure Embedded L4 (seL4) microkernel, designed for real-world use, has potential applications in defence and other safety and security industries where the flawless operation of complex embedded systems is of critical importance.
"It is hard to comment on this achievement without resorting to clichés," says Professor of Computational Logic at Cambridge University's Computer Laboratory, Lawrence C Paulson. "Proving the correctness of 7,500 lines of C code in an operating system's kernel is a unique achievement, which should eventually lead to software that meets currently unimaginable standards of reliability."
"Formal proofs for specific properties have been conducted for smaller kernels, but what we have done is a general, functional correctness proof which has never before been achieved for real-world, high-performance software of this complexity or size," explains NICTA Principal Researcher Dr Gerwin Klein, who leads NICTA's formal verification research team.
(...)
Leia mais em
http://bit.ly/D2Ghf
ou, resumido em português, em
http://www.inovacaotecnologica.com.br/noticias/noticia.php?artigo=primeiro-sistema-operacional-100-livre-erros-esta-pronto&id=010150091020&ebol=sim
Nenhum comentário:
Postar um comentário
Deixe seu comentário! Não uso verificação de palavras.