O modelo Z

O Modelo Z
Eduardo Bráulio Wanderley Netto

Nahri Balesdent Moreano

IC-UNICAMP, CEFET-RN [e-mail] IC-UNICAMP, DCT-UFMS [e-mail] Maio 2001

Resumo
Este trabalho tem como objetivo a apresentação das principais características do método formal Z para especificação de sistemas de computação, incluindo as fases de especificação e validação. Mostramos um exemplo de modelagem de uma máquina de bebidas e finalmente apontamos um conjunto de ferramentas automatizadas que oferecem suporte ao especificador seja na simples apresentação do modelo ou até na prova de teoremas utilizados no processo de validação. O Z se mostrou bastante versátil mas apresenta algumas restrições de uso, especialmente na modelagem de sistemas temporizados.

Abstract
This paper introduces the main features of the Z formal method for specification of computer systems, including the specification and validation stages. We show the modeling of a drink machine as an example and finally we present a set of automated tools which offer support to the specifier including simple viewers of the model, as well as, theorems proof systems which are used in the validation phase. The Z model is versatile but has some constraints of usage, specially in time-dependent systems modeling.

1. Introdução
O alto custo de desenvolvimento e manutenção do software tem levado a uma crescente preocupação com a qualidade do software e com a qualidade do processo de seu desenvolvimento. Desejamos averiguar a qualidade de um sistema em todas as etapas do processo de desenvolvimento, e encontrar erros o mais cedo possível neste processo.
Um dos primeiros estágios no desenvolvimento do software, a engenharia de requisitos, tem papel fundamental no processo de desenvolvimento. Neste estágio elaboramos a especificação dos requisitos do sistema, que servirá de documento base para as etapas seguintes do desenvolvimento.
Erros na especificação de requisitos