UPPAAL

UNIVERSIDADE DE PERNAMBUCO

UPPAAL

UNIVERSIDADE DE PERNAMBUCO

UPPAAL

UPPAAL é um ambiente

integrado de ferramentas para

modelagem, simulação e

verificação de sistemas de

tempo real.

UNIVERSIDADE DE PERNAMBUCO

Universidade de Aalborg, na Dinamarca.

Universidade de Uppsala, na Suécia.

UNIVERSIDADE DE PERNAMBUCO

Universidade de Aalborg, na Dinamarca.

Universidade de Uppsala, na Suécia.

UNIVERSIDADE DE PERNAMBUCO

UPPAAL

UNIVERSIDADE DE PERNAMBUCO

UPPAAL

É adequado para sistemas que podem ser

modelados como um conjunto de processos não

determinísticos com estrutura de controle finito e de

tempo real, se comunicando através de redes ou

variáveis compartilhadas.

UNIVERSIDADE DE PERNAMBUCO

UPPAAL

As áreas de aplicação típicas incluem

controladores em tempo real e os protocolos

de comunicação, em particular projetos onde

o aspecto do tempo é fundamental.

UNIVERSIDADE DE PERNAMBUCO

Licença

A ferramenta UPPAAL é gratuita para

aplicações não-comerciais na acadêmia. Para

aplicações comerciais, é necessária uma

licença comercial.

UNIVERSIDADE DE PERNAMBUCO

Site UPPAAL comercial:

http://www.uppaal.com/

UNIVERSIDADE DE PERNAMBUCO

UPPAAL

UPPAAL consiste em três partes principais:

• uma linguagem de descrição: serve como uma linguagem de

modelagem ou desenho para dscrever o comportamento do sistema;

• um simulador: é uma ferramenta de validação que permite o exame

de possíveis execuções dinâmicas;

• um verificador de modelos: verifica propriedades invariantes e

acessibilidade.

UNIVERSIDADE DE PERNAMBUCO

UPPAAL Editor:

UNIVERSIDADE DE PERNAMBUCO

UPPAAL Simulador:

UNIVERSIDADE DE PERNAMBUCO

UPPAAL Verificador:

UNIVERSIDADE DE PERNAMBUCO

UPPAAL

EFICIÊNCIA FACILIDADE DE USO

UNIVERSIDADE DE PERNAMBUCO

UPPAAL

Para facilitar a modelagem e

depuração, o verificador de

Uppaal pode gerar

automaticamente um diagnóstico

que explica por que uma

propriedade é (ou não é) satisfeita

por uma descrição do sistema.

UNIVERSIDADE DE PERNAMBUCO

UPPAAL

Os vestígios de diagnóstico

gerados pelo verificador

podem ser carregados

automaticamente para o

simulador, o qual pode ser

utilizado para a visualização e

investigação.

UNIVERSIDADE DE PERNAMBUCO

UPPAAL

• A primeira versão da ferramenta foi lançada em 1995 e tem

sido aplicada em uma série de estudos de caso.

• Para atender às exigências decorrentes dos estudos de

caso, a ferramenta foi estendida com várias características.

• A versão atual do UPPAAL foi lançada em 1º de Julho de

2014;

• É uma aplicação implementada em Java e C++, e está

disponível para Linux, SunOS e Windows 7 e 8.

UNIVERSIDADE DE PERNAMBUCO

Site para download da ferramenta:

http://www.uppaal.org/

UNIVERSIDADE DE PERNAMBUCO

Site UPPAAL comercial:

http://www.uppaal.com/

UNIVERSIDADE DE PERNAMBUCO

Download

• É preciso fazer um cadastro para

download da ferramenta, informando

o nome, a universidade e algumas

informações para contato.

• É necessário ter o Java instalado no

computador

(https://www.java.com/pt_BR/download

/).

UNIVERSIDADE DE PERNAMBUCO

Versões disponíveis para download da

ferramenta:

http://www.uppaal.org/

UNIVERSIDADE DE PERNAMBUCO

Pasta Descompactada do UPPAAL:

UNIVERSIDADE DE PERNAMBUCO

Ambiente de trabalho da ferramenta UPPAAL:

UNIVERSIDADE DE PERNAMBUCO

Sintaxe de UPPAAL

A sintaxe usada para declarações UPPAAL é semelhante a

sintaxe utilizada na linguagem de programação C.

• Clocks:

-Sintaxe

- Exemplo:

- clock x , y; Declara dois clocks , x e y.

UNIVERSIDADE DE PERNAMBUCO

Sintaxe

• Variáveis de dados:

- Exemplos:

- int a,b; Inteiro com o domínio default.

- int [0,2] a; Inteiro com o domínio de 0 até 2.

- int b[5]; Array de inteiros.

UNIVERSIDADE DE PERNAMBUCO

Sintaxe

• Ações (Canais):

- Exemplos:

- chan a, b[2]; Canais comuns.

- urgent chan c; Ações Urgentes.

UNIVERSIDADE DE PERNAMBUCO

Sintaxe

• Constantes:

- Exemplos:

- const int [0,1] YES = 1;

- const bool NO = false;

UNIVERSIDADE DE PERNAMBUCO

Declarações

UNIVERSIDADE DE PERNAMBUCO

Declarações

UNIVERSIDADE DE PERNAMBUCO

Templates

• Os autômatos podem ser definidos como um conjunto de

parâmetros que podem ser de qualquer tipo, por exemplo, Int,

Chan. Estes parâmetros são substituídos por um dado

argumento na declaração de processo.

• Templates podem receber parâmetros:

- int v; const min; const max;

• Os templates podem ser instanciados para formar processos:

- P := A (i, 1, 5);

- Q := A (j, 0, 4);

UNIVERSIDADE DE PERNAMBUCO

Invariantes

Uma invariante é uma expressão que satisfaz as seguintes

condições:

• Apenas variáveis inteiras e constantes são referenciados;

• É um conjunto de condições de forma x < x e/ou < = e, onde

x é um clock de referência e “e” avaliada como um inteiro.

UNIVERSIDADE DE PERNAMBUCO

Canais Urgentes

Semântica Informal :

• Não haverá atraso de transição com uma ação urgente;

Restrições:

• Nenhuma restrição de clock é permitida em transições com

ações urgentes.

• Invariantes e restrições de dados de variável são permitidos.

UNIVERSIDADE DE PERNAMBUCO

Broadcast Synchronisation

• Se a é um canal de Broadcast:

a! = Emissão de Broadcast

a? = Recepção de Broadcast

• Em uma transmissão de sincronização um remetente c! pode

sincronizar com um número arbitrário de Receptores c?.

• Um conjunto de arestas em diferentes processos podem sincronizar se

o emissor e o receptor estiverem no mesmo canal.

• Receptores devem sincronizar sempre que possível.

UNIVERSIDADE DE PERNAMBUCO

Mais Expressões

• Lógica:

• && and lógico

• || or lógico

• ! Negação lógica

• Bitwise:

• ^ xor

• & bitwise and

• | bitwise or

• Bit Shift:

• << left

• >> right

• Prefix e Postfix:

• ++ incremento

• -- decremento

• Numérico:

• % módulo

• <? Mínimo

• >? Máximo

• Atribuições:

• += -= != ^= <<= >>=

UNIVERSIDADE DE PERNAMBUCO

Exemplos e Aplicações

UNIVERSIDADE DE PERNAMBUCO

Exemplo

• E – existe um caminho;

• A – para todos os caminhos;

• [] – todos os estados em um caminho;

• <> - alguns estados em um caminho.

Combinaçõe suportadas:

• A[ ], A<>, E<>, E[ ].

UNIVERSIDADE DE PERNAMBUCO

Exemplo

P Reachable – Épossivel alcançar um estado onde P é

satisfeito.

E<> P

UNIVERSIDADE DE PERNAMBUCO

Exemplo

Invariantly P - Dado um estado P, o mesmo é sempre

satisfeito em todos os caminhos.

A[] P

UNIVERSIDADE DE PERNAMBUCO

Exemplo

Inevitable P - Dado um estado P, o mesmo é inevitavelmente

satisfeito em alguns estados e em todos os caminhos.

A<> P

UNIVERSIDADE DE PERNAMBUCO

Exemplo

Potentially Always P - Dado um estado P, existe um

caminho onde P é satisfeito em todos os estaos.

E[] P

UNIVERSIDADE DE PERNAMBUCO

Exemplo

Process 1

idle:

req1=1;

want:

turn=2;

wait:

while(turn!=1 &&

req2!=0);

CS:

//critical section

job1();

req1=0;

//and return to idle

Process 2

idle:

req2=1;

want:

turn=1;

wait:

while(turn!=2 &&

req1!=0);

CS:

//critical section

job2();

req2=0;

//and return to idle

UNIVERSIDADE DE PERNAMBUCO

Exemplo

UNIVERSIDADE DE PERNAMBUCO

Exemplo

UNIVERSIDADE DE PERNAMBUCO

Aplicações utilizando UPPAAL:

http://www.uppaal.com/

UNIVERSIDADE DE PERNAMBUCO

Aplicações ABB – Líder mundial em tecnologias de automação e energia

http://new.abb.com/br/empresa

UNIVERSIDADE DE PERNAMBUCO

Commercial Field Bus Protocol

• Protocolo de comunicação para barramento de campo comercial;

• Desenvolvido e implementado pela ABB para aplicações críticas de

segurança;

• Controle do processo;

• Um dos maiores estudo de caso onde UPPAAL foi aplicado;.

• Falhas na lógica do protocolo e Implementação;

• Fontes de erro são depuradas com base em modelos abstratos do

protocolo;

• Sugestões de melhorias;

Aplicações

UNIVERSIDADE DE PERNAMBUCO

Philips Audio Protocol

• Desenvolvido e implementado pela Philips;

• Troca de informações de controle entre os componentes de um

equipamento de áudio usando codificação Manchester;

• A correção da codificação se baseia em atrasos de tempos entre os

sinais;

• O protocolo é modelado e verificado utilizando UPPAAL.

Aplicações

UNIVERSIDADE DE PERNAMBUCO

Gearbox Controller

• Projeto e análise de um protótipo de controlador de caixa de marchas

de veículos por Mecel AB;

• Componente do sistema distribuído em tempo real que controla um

carro moderno;

• Solicitações de mudança de câmbo Interface homem / máquina

rede de comunicação controlador de caixa de marchas;

• O controlador implementa a mudança de marcha real;

• UPPAAL é aplicado para validar o comportamento do sistema;

• Provas automáticas de 46 propriedades especificados pelo Mecel AB.

Aplicações

UNIVERSIDADE DE PERNAMBUCO

Referências Bibliográficas

• Site: http://www.uppaal.org/

• Site: http://www.uppaal.com/

• UPPAAL Tutorial: http://www.it.uu.se/research/group/darts/papers/texts/new-

tutorial.pdf

• UPPAAL Now, Next and Future:

http://www.it.uu.se/research/group/darts/papers/texts/movep2k.pdf

• Uppaal 4.0: Small Tutorial. A short description of the tool as well as some

examples: http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf