Uma ferramenta para a verificação formal de propriedades de especificações "LOTOS" /

Este trabalho apresenta o desenvolvimento de uma ferramenta para a verificação automatizada de especificações LOTOS. Estas especificações são previamente traduzidas para um modelo intermediário, baseado numa extensão às Redes de Petri. A ferramenta de verificação, que usa a técnica de análise de alc...

ver descrição completa

Na minha lista:
Detalhes bibliográficos
Principais autores: Calderón Sánchez, José Luis., Fialho, Sergio Vianna., Universidade Federal do Rio Grande do Norte.
Formato: Dissertação
Publicado em:
Assuntos:
Redes de computadores.
Sistemas operacionais distribuídos (Computadores).
LOTOS (Linguagem de programação de computador)
Petri, Redes de.
Distributed operating systems (Computers).
Computer network.
Endereço do item:https://app.bczm.ufrn.br/home/#/item/18085
Tags: Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
id oai:localhost:123456789-9731
record_format dspace
spelling oai:localhost:123456789-97312022-11-29T13:38:36Z Uma ferramenta para a verificação formal de propriedades de especificações "LOTOS" / Calderón Sánchez, José Luis. Fialho, Sergio Vianna. Universidade Federal do Rio Grande do Norte. Redes de computadores. Sistemas operacionais distribuídos (Computadores). LOTOS (Linguagem de programação de computador) Petri, Redes de. Distributed operating systems (Computers). Computer network. Este trabalho apresenta o desenvolvimento de uma ferramenta para a verificação automatizada de especificações LOTOS. Estas especificações são previamente traduzidas para um modelo intermediário, baseado numa extensão às Redes de Petri. A ferramenta de verificação, que usa a técnica de análise de alcançabilidade, cria e expande parcialmente um grafo relacionado ao comportamento do sistema especificado, de maneira a evitar o problema da "explosão" do espaço de estados. Uma técnica heurística é usada, em conjunto com a estratégia de busca "best first", para guiar a geração do grafo em direção à solução esperada. Esta técnica associa aos eventos oferecidos pelo sistema uma estimativa do custo para se atingir o estado objetivo, onde a propriedade se verifica. As propriedades do sistema são traduzidas em listas de condições, avaliadas segundo uma sequência determinada. É ainda apresentada a verificação de cinco propriedades do protocolo de transmissão de mensagens "Bit Alternado", ilustrando "passo a passo" o processo de verificação feito pela ferramenta.#$&This work presents the development of a tool for the automated verification of LOTOS specifications. These specifications are previously translated to an intermediate model, based on an extension of Petri Nets. The verification tool, using a reachability analysis technique, creates and expands a partial graph related to the behavior of the specified system, in order to avoid the state space "explosion" problem. A heuristic technique is used, in association with a "best-first" search strategy, to guide the graph generation towards the expected solution. It assigns to each event offered by the system an estimate of the cost to reach the objective state, where property is verified. The system properties are translated to a condition list, and are evaluated in a determined sequence. Five properties for the "Alternating Bit" protocol are presented, to ilustrated, step by step, the verification process executed by the verification tool. 1 2022-10-04T17:31:37Z 2022-10-04T17:31:37Z 1995. Dissertação 681.3 C146f DISSERT 18085 https://app.bczm.ufrn.br/home/#/item/18085 https://app.bczm.ufrn.br/home/#/item/18085
institution Acervo SISBI
collection SIGAA
topic Redes de computadores.
Sistemas operacionais distribuídos (Computadores).
LOTOS (Linguagem de programação de computador)
Petri, Redes de.
Distributed operating systems (Computers).
Computer network.
spellingShingle Redes de computadores.
Sistemas operacionais distribuídos (Computadores).
LOTOS (Linguagem de programação de computador)
Petri, Redes de.
Distributed operating systems (Computers).
Computer network.
Calderón Sánchez, José Luis.
Fialho, Sergio Vianna.
Universidade Federal do Rio Grande do Norte.
Uma ferramenta para a verificação formal de propriedades de especificações "LOTOS" /
description Este trabalho apresenta o desenvolvimento de uma ferramenta para a verificação automatizada de especificações LOTOS. Estas especificações são previamente traduzidas para um modelo intermediário, baseado numa extensão às Redes de Petri. A ferramenta de verificação, que usa a técnica de análise de alcançabilidade, cria e expande parcialmente um grafo relacionado ao comportamento do sistema especificado, de maneira a evitar o problema da "explosão" do espaço de estados. Uma técnica heurística é usada, em conjunto com a estratégia de busca "best first", para guiar a geração do grafo em direção à solução esperada. Esta técnica associa aos eventos oferecidos pelo sistema uma estimativa do custo para se atingir o estado objetivo, onde a propriedade se verifica. As propriedades do sistema são traduzidas em listas de condições, avaliadas segundo uma sequência determinada. É ainda apresentada a verificação de cinco propriedades do protocolo de transmissão de mensagens "Bit Alternado", ilustrando "passo a passo" o processo de verificação feito pela ferramenta.#$&This work presents the development of a tool for the automated verification of LOTOS specifications. These specifications are previously translated to an intermediate model, based on an extension of Petri Nets. The verification tool, using a reachability analysis technique, creates and expands a partial graph related to the behavior of the specified system, in order to avoid the state space "explosion" problem. A heuristic technique is used, in association with a "best-first" search strategy, to guide the graph generation towards the expected solution. It assigns to each event offered by the system an estimate of the cost to reach the objective state, where property is verified. The system properties are translated to a condition list, and are evaluated in a determined sequence. Five properties for the "Alternating Bit" protocol are presented, to ilustrated, step by step, the verification process executed by the verification tool.
format Dissertação
author Calderón Sánchez, José Luis.
Fialho, Sergio Vianna.
Universidade Federal do Rio Grande do Norte.
author_facet Calderón Sánchez, José Luis.
Fialho, Sergio Vianna.
Universidade Federal do Rio Grande do Norte.
author_sort Calderón Sánchez, José Luis.
title Uma ferramenta para a verificação formal de propriedades de especificações "LOTOS" /
title_short Uma ferramenta para a verificação formal de propriedades de especificações "LOTOS" /
title_full Uma ferramenta para a verificação formal de propriedades de especificações "LOTOS" /
title_fullStr Uma ferramenta para a verificação formal de propriedades de especificações "LOTOS" /
title_full_unstemmed Uma ferramenta para a verificação formal de propriedades de especificações "LOTOS" /
title_sort uma ferramenta para a verificação formal de propriedades de especificações "lotos" /
publishDate 2022
url https://app.bczm.ufrn.br/home/#/item/18085
work_keys_str_mv AT calderonsanchezjoseluis umaferramentaparaaverificacaoformaldepropriedadesdeespecificacoeslotos
AT fialhosergiovianna umaferramentaparaaverificacaoformaldepropriedadesdeespecificacoeslotos
AT universidadefederaldoriograndedonorte umaferramentaparaaverificacaoformaldepropriedadesdeespecificacoeslotos
_version_ 1766805312389513216

Registros relacionados