Realidades Paralelas

Wednesday, July 27, 2005

Mais sobre lógica e formalização

During the last 10 years we have seen a number of failures in these kind of systems. I just mention four well-known examples.

The first example is the Ariadne rocket, a common European space project. The rocket exploded a few seconds after takeoff, due to a software error.

Another well known example is the baggage-handling system of the Denver International Airport. Errors in the software that controls the system required postponement of the official opening (Oct. 1993). By June 1994 the $193 million system was still not functioning, but costing $1.1 million per day in interest and other costs. In early 1995 a manual baggage system was installed in order to open the airport.

Some cancer patients in the USA have received fatal radiation overdoses from the Therac-25, a computer-controlled radiation-therapy machine.

The last example is the Sizewell B nuclear power plant in England. Some years ago it was decided to test the subsystem which is used to close down the reactor if a dangerous situation occurs. The results were not comforting: the software failed almost half of them. They were not able to find the errors in the 100,000 lines of code. Instead, they reduced the overall expectation of the plant's performance from one failure every 10,000 years to one every 1,000 years.

Esses são exemplos de sistemas críticos, nos quais foi investido muito dinheiro e que mesmo assim foram fracassos consideráveis. Não são os únicos exemplos: Larry Paulson menciona, nas notas de um de seus cursos, um sistema de controle de ambulâncias na Inglaterra que causou a morte de vários pacientes por atraso de atendimento. Tendo em vista isso, é fácil concordar que essa tal engenharia de software deixa muito a desejar. Será que eu sou o único a achar loucura confiar em sistemas assim ?

O trecho é de uma palestra proferida por Bengt Nordstrom em um evento no Vaticano. Sigam o link e leiam a coisa toda, é interessante.

1 Comments:

  • Em uma aula de Engenharia de Software (que tive há alguns semestres), o professor usou esse exemplo do fogete Ariadne. O engraçado é que as "soluções" propriamente ditas não garantiam que esse tipo de problema fosse eliminado. Na verdade, a solução apontada pelo professor, como a única que garantia corretude, era "modelar" o problema/objeto em questão utilizando também cálculo lambda, além do código propriamente dito. Bom, no fundo isso não garante nada, porque o código original pode estar diferente da versão remodelada. Curiosamente, quando perguntado sobre técnicas de engenharia de projeto em linguagens funcionais, ele disse que desconhecia alguma.

    A minha conclusão disso tudo, é basicamente o que você falou. Quem sabe, um dia, a computação vai parar de ser arte e se tornar ciência. :)

    E é isso.

    By Anonymous Anonymous, at 9:01 AM  

Post a Comment

<< Home