Submitted by JÚLIO HEBER SILVA (julioheber@yahoo.com.br) on 2017-04-11T19:28:47Z No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2017-04-12T14:32:03Z (GMT) No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2017-04-12T14:32:03Z (GMT). No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2017-03-07 / Fundação de Amparo à Pesquisa do Estado de Goiás - FAPEG / The process of developing computer systems takes into account many stages, in which some are more necessary than others, depending on the purpose of the application. The implementation stage is always necessary, indisputably. Sometimes the requirements analysis and testing phases are neglected. And, generally, the part of formal verification correctness is intended for few applications. The use of model checkers has been exploited in the task of validating a behavioral specification in its appropriate level of abstraction, notably specifications validation of critical systems, especially when they involve the preservation of human life, when the existence of errors entails huge financial loss or when deals with information security. Therefore, it proposes to apply formal verification techniques in the validation of the vehicular safety system Avoiding Doored System, considered as critical, in order to verify if the implemented system faithfully meets the requirements for it proposed. For that, it was used as a tool to verify its correctness the Specification and Verification System - PVS, detailing and documenting all the steps employed in the process of specification and formal verification. K / O processo de desenvolvimento de sistemas computacionais leva em conta muitas etapas, nos quais umas são tidas mais necessárias que outras, dependendo da finalidade da aplica- ção. A etapa de implementação sempre é necessária, indiscutivelmente. Por vezes as fases de análise de requisitos e de testes são negligenciadas. E, geralmente, a parte de verifica- ção formal de corretude é destinada a poucas aplicações. 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. Diante disso, se propõe aplicar técnicas de verificação formal na validação do sistema de segurança veicular Avoiding Doored System, tido como crítico, com o intuito de atestar se o sistema implementado atende, fielmente, os requisitos para ele propostos. Para tal, foi utilizada como ferramenta para a verificação de sua corretude o Specification and Verification System - PVS, detalhando e documentando todas as etapas empregadas no processo de especificação e verificação formal. Pal