Atenção: Todas as denúncias são sigilosas e sua identidade será preservada.
Os campos nome e e-mail são de preenchimento opcional
Metadados | Descrição | Idioma |
---|---|---|
Autor(es): dc.contributor | Lopes, Bruno | - |
Autor(es): dc.contributor | Carvalho, Aline Marins Paes | - |
Autor(es): dc.contributor | Santos, Jefferson de Barros | - |
Autor(es): dc.creator | Toledo, Daniel Arena | - |
Data de aceite: dc.date.accessioned | 2024-07-11T18:48:02Z | - |
Data de disponibilização: dc.date.available | 2024-07-11T18:48:02Z | - |
Data de envio: dc.date.issued | 2023-11-15 | - |
Data de envio: dc.date.issued | 2023-11-15 | - |
Fonte completa do material: dc.identifier | http://app.uff.br/riuff/handle/1/31123 | - |
Fonte: dc.identifier.uri | http://educapes.capes.gov.br/handle/capes/777849 | - |
Descrição: dc.description | Sistemas 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.description | Critical 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.description | 87 p. | - |
Formato: dc.format | application/octet-stream | - |
Formato: dc.format | application/pdf | - |
Idioma: dc.language | pt_BR | - |
Direitos: dc.rights | Open Access | - |
Direitos: dc.rights | CC-BY-SA | - |
Palavras-chave: dc.subject | Verificação de modelos | - |
Palavras-chave: dc.subject | Reo | - |
Palavras-chave: dc.subject | Constraint Automata | - |
Palavras-chave: dc.subject | NuXmv | - |
Palavras-chave: dc.subject | Lógica proposicional | - |
Palavras-chave: dc.subject | Linguagem de programação (Computador) | - |
Palavras-chave: dc.subject | Teste (Computação) | - |
Título: dc.title | Um compilador de circuitos Reo para modelos nuXmv | - |
Tipo de arquivo: dc.type | Trabalho de conclusão de curso | - |
Aparece nas coleções: | Repositório Institucional da Universidade Federal Fluminense - RiUFF |
O Portal eduCAPES é oferecido ao usuário, condicionado à aceitação dos termos, condições e avisos contidos aqui e sem modificações. A CAPES poderá modificar o conteúdo ou formato deste site ou acabar com a sua operação ou suas ferramentas a seu critério único e sem aviso prévio. Ao acessar este portal, você, usuário pessoa física ou jurídica, se declara compreender e aceitar as condições aqui estabelecidas, da seguinte forma: