A crescente demanda para a evolução do software, em função da disponibilidade de hardware mais avançado, gerou a necessidade da criação de técnicas e metodologias para suportarem esta investida. Desde então surgiram várias técnicas, da Análise Estruturada nos anos 70 às metodologias Orientadas a Objetos nos anos 90. Para a Engenharia de Software tornou-se extremamente importante a fusão destas técnicas, primeiro pelo ganho das metodologias resultantes e segundo pela introdução da padronização dos modelos destes sistemas. Como resultado das fusões de diversos métodos surgiu o Processo Unificado de Desenvolvimento de Software, que utiliza a UML como sendo uma linguagem de modelagem para especificação, construção e documentação de seus modelos. Essa linguagem permitiu que a tarefa de análise e eliciação de requisitos se tornasse mais disciplinada, além de uma aproximação maior com o usuário, que é quem melhor entende do processo de negócio do sistema em desenvolvimento. Em função da informalidade desta fase, tornou-se mais difícil o processo de validação dos requisitos do sistema, uma vez que erros de modelagem nas fases preliminares identificados mais adiante têm um custo muito elevado, proporcionalmente ao tamanho e à complexidade do sistema. Esta dificuldade se agrava ainda mais quando consideramos os Sistemas de Informação para a Automação, que demandam uma integração vertical entre os processos gerenciais e as atividades de chão de fábrica. Com o objetivo de tornar possível a minimização do número de erros na fase de requisitos, neste trabalho será apresentada uma proposta que transforma os requisitos em especificação formal. Este processo é apresentado como sendo um refinamento da descrição disciplinada dos Use Cases, utilizando Redes de Petri como linguagem formal e ferramenta de validação.

The availability of hardware facilities for computer systems has increased the demand for large software and generated the need for new techniques and methodologies to support this offensive. Several paradigms have appeared, from the Structured Analysis in the 70's to Objects Orientation in the 90's. The fusion of these techniques are extremely important for Software Engineering, first because of the increased potential of the resulting methodologies, and second by the introduction of standard models for the target systems. The Unified Software Development Process is the most accepted result of the fusion method concerning object-oriented approaches, which have defined the UML as a language of modeling for specification, construction and documentation of systems. The language also allows that Requirements Elicitation and Analysis could be disciplined always centered in the user who understands better the business process. Due to the informality of the first step in the life cycle, the validation of the system requirements became more difficult, leading to very costly errors, which are proportional to the size and complexity of the project. Such difficulty becomes even worst when we consider Information Systems for Automation as a target. These systems demand a vertical integration between the management processes and shop floor activities. The requirements phase's errors can be minimized by the conversion in formal specification of the systemsrequirements, which is the proposal of this work. This process is presented as a Use Cases specification refinement, by using Petri net as formal language and verification tool.