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, 2010 / Made available in DSpace on 2012-10-25T03:15:55Z (GMT). No. of bitstreams: 1
287047.pdf: 2105803 bytes, checksum: a722cc55acdfaf3252bdf60d781f04b3 (MD5) / Para resolver os problemas associados a verificação de sistemas industriais complexos, como os desenvolvidos para CLPs, são necessárias técnicas de modelagem e verificação formal, como forma de provar que o programa está de acordo com as propriedades esperadas. Neste trabalho é proposto um modelo de tradução da linguagem Diagrama Ladder de CLPs para uma linguagem intermediária de verificação FIACRE, que está inserida em uma cadeia de verificação formal do projeto Topcased. Esta abordagem segue o paradigma da engenharia dirigida a modelos e consiste em transformar modelos próximos ao usuário em modelos para a verificação. As regras de transformação propostas devem estar inseridas em duas cadeias de verificação formal, que utilizam as abordagens de model-checking e por equivalências de modelos. A validação da proposta é feita por intermédio da transformação de modelos e verificação das propriedades de um sistema de automação pneumática e um sistema para um misturador industrial.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufsc.br:123456789/93771 |
| Date | 25 October 2012 |
| Creators | Souza, Mateus Feijó de |
| Contributors | Universidade Federal de Santa Catarina, Farines, Jean Marie, Queiroz, Max Hering de |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | xxiii, 162 p.| il., tabs. |
| 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.0022 seconds