NICTA today announced the completion of the world’s first formal machine-checked proof of a general-purpose operating system kernel, promising safety-critical software of unprecedented levels of reliability.
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 ========================================== Adolfo Neto Departamento Acadêmico de Informática Universidade Tecnológica Federal do Paraná Fone: (41) 3310-4644 / Fax: (41) 3310-4646 Web: http://www.dainf.ct.utfpr.edu.br/~adolfo Blog: http://professoradolfo.blogspot.com ==========================================
_______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
