Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pòs-graduação em Engenharia de Automação e Sistemas, Florianópolis, 2011 / Made available in DSpace on 2012-10-26T05:05:01Z (GMT). No. of bitstreams: 1
296872.pdf: 1897409 bytes, checksum: 109437d10a6b10646d5638bb03afd255 (MD5) / projeto de sistemas embarcados criticos exige o uso de metodologias adequadas, visto que falhas no sistema podem causar danos catastroficos. Neste contexto se enquadra o projeto Topcased, o qual propõe uma série de ferramentas capazes de suportar a verificação formal de propriedades. A linguagem AADL tem um papel fundamental neste processo, pois sua utilização permite o emprego da transformação de modelos e a aplicação da verificação formal de propriedades. Entretanto, a especificação das propriedades de verificação e a análise dos seus resultados são ainda topicos em aberto. Esta dissertação visa suprir esta carência propondo um assistente para especificação de propriedades de verificação na linguagem AADL e uma interface para a visualização dos resultados de verificação, juntamente com um simulador de contraexemplos. O assistente construido classica as propriedades em padrões pre-definidos, utilizando uma linguagem natural ao usuário. Para validar as ferramentas desenvolvidas realizou-se um estudo de caso, o qual consistiu da especificação e verificação de propriedades de um sistema de marcapasso. Desta forma, este trabalho contribui com a melhoria da cadeia de verificação da linguagem AADL no escopo do projeto Topcased.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufsc.br:123456789/95694 |
| Date | 26 October 2012 |
| Creators | Oliveira, Rafael Garlet de |
| Contributors | Universidade Federal de Santa Catarina, Becker, Leandro Buss, Farines, Jean Marie |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | xxviii, 188 p.| il. |
| Source | reponame:Repositório Institucional da UFSC, instname:Universidade Federal de Santa Catarina, instacron:UFSC |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0017 seconds