Verificação formal de sistemas digitais embarcados
SILVA, Nayara de Souza ; COSTA, Vaston Gonçalves da ; Stoppa, Marcelo Henrique
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).
34 downloads
DOI: 10.5151/9788580392234-08
Como citar:
SILVA, Nayara de Souza; COSTA, Vaston Gonçalves da; STOPPA, Marcelo Henrique; "Verificação formal de sistemas digitais embarcados", p. 121-134. Tecnologias em pesquisa: engenharias. São Paulo: Blucher, 2017.
ISBN: 9788580392234, DOI 10.5151/9788580392234-08