| |
| Acadêmico(a): Bruno Biribio Woerner |
| Título: Um Estudo de Caso Usando o Método Formal Z para Especificação de um Sistema |
| |
| Conclusão: |
| Desenvolver uma especificação formal a partir de uma notação não conhecida, não é uma das tarefas mais triviais. A curva de aprendizado para utilizar os conceitos e construções é relativamente grande e morosa. Mesmo utilizando da ferramenta Z/EVES para construção da especificação, a especificação do sistema é trabalhosa e exige muita dedicação. O objetivo principal deste trabalho foi alcançado. A utilização de uma especificação formal no desenvolvimento de sistemas foi largamente discutido no trabalho. A implementação torna-se mais compreensiva e provê um maior dinamismo ao implementar um sistema a partir de uma especificação escrita em Z, mostrando que esta foi de grande valia na fase de implementação. A notação Z seria mais bem aproveitada caso existisse um ferramental mais completo que proporcionasse a construção de especificações e templates de códigos para a especificação construída. Os requisitos do sistema de biblioteca foram executados com sucesso, tanto as funções de cadastro e manipulação dos objetos, como os relatórios e funções. Todos foram especificados com a notação Z e implementados em Java. Na parte de testes, a especificação em Z mostrou-se de grande viabilidade. Desenvolver testes utilizando da especificação formal mostrou-se muito mais eficiente do que técnicas tradicionais. A especificação trouxe clareza e segurança ao implementar os testes. A utilização de prova de propriedades não foi amplamente utilizada, porém foi demonstrado que é possível sim utilizar das propriedades matemáticas. A prova possibilita garantir que o especificado é ou não consistente. O roteiro de uso que se propôs inicialmente não foi construído. Para isso, é necessário um maior aprofundamento no assunto para não ser apenas uma compilação de boas práticas no processo de desenvolvimento. Certamente, a construção de uma metodologia para desenvolvimento utilizando especificação formal é mais viável e agrega mais valor. Resta concluir que especificação formal é sim viável e útil. Com o aprendizado, experiência adquirida e ferramental adequado é muito mais produtivo e simples realizar a implementação de um sistema. |
| |
|
