Resumo:

O uso de verificadores de modelos tem sido explorado na tarefa de validar uma especificação comportamental no seu nível adequado de abstração, sobretudo, na validação de especificações de sistemas críticos, principalmente quando estes envolvem a preservação da vida humana, quando a existência de erros acarreta enorme prejuízo financeiro, ou quando tratam com a segurança da informação. Neste artigo é apresentado um arcabouço metodológico prático para tratar da implementação de procedimentos a serem empregados na especificação formal de sistemas. Como estudo de caso, trabalhou-se com o sistema digital embarcado Avoiding Doored System (ADS), tido como crítico, cuja corretude fora verificada formalmente utilizando-se como ferramenta semi automática o Specification and Verification System (PVS).