Modelagem e verificação automática de um protocolo de controle de fluxo adaptativo usando traços de execução.

• Ano de defesa: 2016
• Autor(a) principal: MOREIRA, Anne Lorayne Gerônimo Silva Augusto.
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal de Campina Grande; Brasil; Centro de Engenharia Elétrica e Informática - CEEI; PÓS-GRADUAÇÃO EM CIÊNCIA DA COMPUTAÇÃO; UFCG
• Palavras-chave em Português: Verificação Formal; Verificação Automática; Sistemas Embarcados; Modelos Formais; NuSMV; Formal Verification; Automatic Verification; Embedded Systems; Formal Models; Ciências; Ciência da Computação
• Link de acesso: http://dspace.sti.ufcg.edu.br:8080/jspui/handle/riufcg/768

O desenvolvimento de sistemas embarcados possibilitou uma forte expansão no número de aplicações dependentes de dispositivos programáveis em áreas tão distintas como automobilística, sistemas financeiros e sistemas médicos. Uma eventual falha em algum desses sistemas pode provocar diferentes graus de danos e prejuízos e, por isso, exige-se um alto grau de confiabilidade em seu funcionamento. O aumento da complexidade dos novos sistemas computacionais e a pressão econômica e busca de novos mercados, concorrem para a busca da redução nos prazos de entrega dos dispositivos programáveis e de seus softwares e sistemas embarcados. Este trabalho apresenta um estudo de caso para a utilização de um método de verificação formal de software aplicado a um sistema computacional de controle de fluxo adaptativo para Gateways Bluetooth Low-Energy utilizados em sistemas de monitoramento remoto de pacientes. Os resultados obtidos neste trabalho confirmam a viabilidade da aplicação do método na verificação formal do software proposto.