Verificação de propriedades de sistemas híbridos modelados com redes de petri

UNIVERSIDADE FEDERAL DO CEARÁ CURSO DE ENGENHARIA DA COMPUTAÇÃO

Resumo da tese “Verificação de Propriedades de Sistemas Híbridos”

Ceará
2013

O modelo de um sistema é caracterizado pela natureza de suas variáveis de estado e da variável independente que representa o tempo. Existem dois tipos de variáveis, as discretas e as continuas. Nos sistemas de variáveis contínuas, o conjunto de variáveis que representa seu estado evolui de forma continua no tempo.
Já nos sistemas de eventos discretos, as variáveis de estado são modificadas de acordo com a ocorrência de eventos instantâneos. Seus valores permanecem constantes entre a ocorrência de eventos.
Os sistemas híbridos são formados por variáveis de natureza continuas e variáveis de natureza discreta. Logo, sistemas híbridos são sistemas nos quais o comportamento é determinado pela interação entre as duas dinâmicas: contínua e evento discreto.
Como exemplo de modelagem de sistemas híbridos, o artigo usa uma rede de sensores sem fio. Que é composta por micro-sensores compactos com capacidade de comunicação sem fio. Tais sensores são dispositivos autômatos e compactos e serão chamados de nós sensores e seu funcionamento é da seguinte forma:
1. Os nós sensores coletam os dados.
2. Os nós sensores encaminham os dados para o nó sink usando uma estrutura sem fio
3. O nó sink se comunica com o nó gerenciador de tarefas via internet ou satélite
Os nós sensores possuem as seguintes características: deve ser eficiente no uso de energia, deve ser de baixo custo, deve proporcionar um sensoriamento distribuído, deve usar comunicação sem fio, deve usar caminhos multi-hop para o envio de informações e deve possuir processamento distribuído.
Os nós sensores de uma rede de sensores sem fio possuem quatro subdivisões: subsistema de fonte de energia; subsistema de sensoriamento e atuação; subsistema computacional e subsistema