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
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.bc.ufg.br:tede/7134 |
| Date | 07 March 2017 |
| Creators | Silva, Nayara de Souza |
| Contributors | Costa, Vaston Gonçalves da, Stoppa, Marcelo Henrique, Costa, Vaston Gonçalves da, Galdino, André Luiz, Rabelo, Marcos Napoleão |
| Publisher | Universidade Federal de Goiás, Programa de Pós-graduação em Modelagem e Otimização (RC), UFG, Brasil, Regional Catalão (RC) |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Biblioteca Digital de Teses e Dissertações da UFG, instname:Universidade Federal de Goiás, instacron:UFG |
| Rights | http://creativecommons.org/licenses/by-nc-nd/4.0/, info:eu-repo/semantics/openAccess |
| Relation | 5321942601948699525, 600, 600, 600, 600, 6665988530194015545, -7090823417984401694, -961409807440757778 |
Page generated in 0.0031 seconds