Um compilador de circuitos Reo para modelos nuXmv

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.contributorLopes, Bruno-
Autor(es): dc.contributorCarvalho, Aline Marins Paes-
Autor(es): dc.contributorSantos, Jefferson de Barros-
Autor(es): dc.creatorToledo, Daniel Arena-
Data de aceite: dc.date.accessioned2024-07-11T18:48:02Z-
Data de disponibilização: dc.date.available2024-07-11T18:48:02Z-
Data de envio: dc.date.issued2023-11-15-
Data de envio: dc.date.issued2023-11-15-
Fonte completa do material: dc.identifierhttp://app.uff.br/riuff/handle/1/31123-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/capes/777849-
Descrição: dc.descriptionSistemas críticos necessitam de alto nível de confiança e estão presentes em vários lugares na atualidade. Muitas vezes a validação desses sistemas é uma tarefa árdua e que requer muito esforço. Reo é uma linguagem gráfica baseada em coordenações que procura modelar a interação entre componentes num sistema, facilitando assim a modelagem desses tipos de sistemas. Constraint Automata é um formalismo usado para se raciocinar acerca de Reo, podendo-se assim validar propriedades desses modelos. Dentre as ferramentas disponíveis para validação de sistemas, o nuXmv se propõe como um verificador de modelos simbólico que verifica formalmente propriedades acerca de um modelo. Este trabalho implementa uma ferramenta que compila um circuito Reo para um modelo nuXmv, facilitando assim o processo de validação desses tipos de sistemas. As funcionalidades da ferramenta, a teoria utilizadas e alguns exemplos de usos são apresentados neste trabalho-
Descrição: dc.descriptionCritical systems require a high level of reliability and are present in many scenarios. Validating these systems is an arduous and time consuming task. Reo is a graphical language based on coordination that aims to model the interaction between components in a system, thus facilitating the modeling of these types of systems. Constraint Automata is a formalism used to reason about Reo, thus being able to validate properties of these models. Among the tools available for system validation, nuXmv is as a symbolic model checker that formally verifies properties about a model. This work implements a tool that compiles a Reo circuit for a nuXmv model, thus facilitating the validation process of these types of systems. The functionalities of the tool, the theory used and some examples of uses are presented in this work-
Descrição: dc.description87 p.-
Formato: dc.formatapplication/octet-stream-
Formato: dc.formatapplication/pdf-
Idioma: dc.languagept_BR-
Direitos: dc.rightsOpen Access-
Direitos: dc.rightsCC-BY-SA-
Palavras-chave: dc.subjectVerificação de modelos-
Palavras-chave: dc.subjectReo-
Palavras-chave: dc.subjectConstraint Automata-
Palavras-chave: dc.subjectNuXmv-
Palavras-chave: dc.subjectLógica proposicional-
Palavras-chave: dc.subjectLinguagem de programação (Computador)-
Palavras-chave: dc.subjectTeste (Computação)-
Título: dc.titleUm compilador de circuitos Reo para modelos nuXmv-
Tipo de arquivo: dc.typeTrabalho de conclusão de curso-
Aparece nas coleções:Repositório Institucional da Universidade Federal Fluminense - RiUFF

Não existem arquivos associados a este item.