| |
| Acadêmico(a): Bruno Biribio Woerner |
| Título: Um Estudo de Caso Usando o Método Formal Z para Especificação de um Sistema |
| |
| Introdução: |
| Moura (2001, p. 25-27) descreve o uso de métodos formais como meio de evitar falhas em módulos de software, além de proporcionar auxílio no processo de desenvolvimento. Atualmente a tecnologia de projeto e produção de hardware possui um elevado grau de sofisticação, resultando em um número muito baixo de falhas nestes componentes. Há uma rigorosidade muito maior na produção de hardware com relação a sua especificação. Nos sistemas computacionais o limitador de progresso não está atrelado ao hardware, o software é o maior responsável por este título. Erros e comportamentos indesejados no software servem de embasamento para esta afirmação. O método formal por sua vez objetiva evitar ao máximo que falhas ocorram, permitindo que o comportamento de um programa possa ser conhecido e analisado sem que haja a necessidade de executar seu código fonte. Davies e Woodcock (1996, p. 1-2) apresentam os métodos atuais de especificação de software como ambíguos, imprecisos e focados em detalhes não importantes ao produto em si. Esta ambigüidade acarreta em descobrir alguns problemas muito tardiamente e muitas vezes inviabiliza o projeto em plena construção. Para resolver este problema é necessário utilizar-se de uma linguagem sem ambigüidade, precisa e com um bom nível de abstração. Estas características remetem à matemática. Os métodos formais são fortemente baseados em toda a ciência matemática. Conforme Moura (2001, p. 30-31), a notação formal Z é apropriada para este cenário. Baseada fortemente na teoria dos conjuntos demonstra uma maneira precisa e simples de especificar um software. A notação Z não é uma simples tradução de texto para fórmulas matemáticas, mas sim uma maneira de apresentar o comportamento e propriedades do software. Z não é executável, a definição pode ser construída de diversas formas a fim de proporcionar diferentes métodos de construção. Ainda, segundo Spivey (1992, p. 128), a mais complexa das definições realizadas em Z não é nada mais que teoria matemática organizada de uma maneira estruturada. Potter, Sinclair e Till (1996, p. 309) explicam que o ganho em precisão na especificação utilizando Z proporciona uma redução considerável na quantidade de erros no processo de produção do software, que provavelmente seriam descobertos em fases futuras do processo de desenvolvimento ou de implantação. Isso é facilmente evidenciado em virtude do desenvolvedor possuir o prévio conhecimento do software e do que necessita ser testado. A partir do exposto, são apresentadas neste trabalho a especificação e a implementação de um estudo de caso utilizando a notação Z, detalhando cada passo, objetivando demonstrar a validade e consistência dos requisitos de um sistema. Ainda, segundo Moura (2001, p. 32) pode-se “agregar à especificação técnicas para prova de propriedades acerca do objeto especificado, caminhando na direção de um cálculo de programas.” Também será disponibilizado um roteiro de uso enfocando um sistema desde a sua especificação até a implementação. O sistema de biblioteca foi a aplicação escolhida para ser desenvolvida utilizando a notação Z. Hall (1990, p. 15) afirma que métodos formais podem ser aplicados em qualquer tipo de software. |
| |
|
