Universidade Federal da Bahia

Com a crescente utilização da informática em nossas vidas, é cada vez maior a nossa dependência nos programas de computadores. Não é exagero afirmar que em muitas situações nossas vidas dependem de programas de computadores. Como exemplos de sistemas críticos, podemos mencionar os programas que controlam a dosagem de radiação aplicada a um paciente em tratamento radioterápico, os vários programas controlam o reator de uma usina nuclear, o uso de programas e computadores em aviões, bem como em sistemas de transportes públicos, como trens e metrôs. Uma falha em programas como os acima citados podem levar a grandes perdas econômicas, e o que é pior, podem causar também perdas de vidas. Segundo Bertrand Meyer, “se um sistema não faz aquilo que ele deveria fazer, então muito pouco resta de relevância sobre ele”. Entre todos os critérios de qualidade de software, corretude é o mais fundamental. Trata-se de um conceito intrinsecamente relativo, uma vez que requer uma referencia. Dizer que um sistema é correto, significa afirmar que sua implementação é consistente, ou satisfaz, a sua especificação (a referência). Um método de desenvolvimento de sistemas que permite a definição precisa de um problema, e avança em direção a uma implementação que é provada correta em relação à dada especificação, é considerado formal. A pré-condição necessária para assegurar a corretude é basear o processo de desenvolvimento de um sistema em um método formal. O MEFES visa a proposição de processos de desenvolvimento de softwares que sejam sistemáticos, baseados em métodos e ferramentas, e aplicáveis a sistemas reais. Tendo sempre em mente a produção de software de qualidade, focando principalmente no aspecto de corretude, dentro de limites previsíveis de tempo e custo.

GT-Projetos STI

GT-Projetos STI