[FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto - OFF

[Paulo Henrique]

É isso ai lista continuamos a thread... pois a aula está muito
interessante...

2009/10/26 Jean Everson Martina <everson em inf.ufsc.br>

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
>
> > Um pequeno programa é uma exceção. Algum programa (como esse que você
> > falou, talvez), com o espírito acadêmico (principalmente), pode tratar
> > exceções. O que não deixa de ter validade empírica, mesmo sabendo da
> > existência do Teorema da Parada.
>
> Você esta confundido a abrangência do teorema de parada. Ele diz que não
> existe algorítimo genérico para decidir a parada para todos os pares
> entrada-programa. O que não quer dizer que não existe solução para casos
> específicos.
>
> Sobre a validade empírica, você pode explicar o que é uma validade
> formal então?
>
> De novo, se você estiver correto de que tudo é empírico, um player como
> a MS, não investiria mais de 2 milhões de libras no projeto Terminator
> (o que prova que não é brincadeirinha acadêmica):
>
>
> http://research.microsoft.com/en-us/um/cambridge/projects/terminator/default.htm
>
> O Terminator é um dos maiores responsáveis pelo aumento de estabilidade
> do XP, Vista e 7. Você vê hoje muito menos telas azuis e crashes, porque
> o drivers certificados foram sendo verificados quanto a não parada. Sim,
> se está longe de ter a verificação formal completa de um SO de uso
> genérico. Mas eu digo que em 15 anos isso será um fato.
>
> Na verdade, tem outros projetos semelhantes sobre verificação de chips
> usando métodos automatizados e logica de ordem mais alta, que são usados
> pela ARM (100% do que a ARM faz é verificado formalmente, e eles são a
> maior plataforma de Micro-processadores hoje). A Intel e AMD também
> fazem mas não em 100% dos casos.
>
> Aqui mesmo (Grupo de Teoria da Computação de Cambridge), temos projetos
> com a NSA pra verificação formal de micro-processadores criptográficos,
> , com a Cisco e Boeing na área de roteamento, com a IBM na área de
> módulos java e com a Intel na verificação de assembly x86, etc
>
> Meu PhD é sobre verificação formal de protocolos criptográficos, onde
> parte da pesquisa já foi bancada pela VISA (verificação do SET) e pelo
> Internet Consortium (Verificação do SSL). Hoje o governo brasileiro (que
> me banca) tem interesse em verificar os grandes protocolos no cenário
> nacional, tais como SPB, NF-e e OpenHSM. É por isso que eu to aqui.
>
> Sobre uma outra pergunta na discussão sobre a usabilidade deste
> microkernel: Sim ele é utilizável e funcional, mas dentro da plataforma
> e objetivos à que se propõe.
>
>
> Jean
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.4.8 (Darwin)
> Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
>
> iEYEARECAAYFAkrldh0ACgkQQN0Max56Wid4KwCggkNfAxKzj/B5oLBn4Bt1uPty
> Ow0AoKbvPMBAmEbKWTe6eQHsN45ULGP8
> =CheR
> -----END PGP SIGNATURE-----
> -------------------------
> Histórico: http://www.fug.com.br/historico/html/freebsd/
> Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
>