Upload
mayara-monica
View
175
Download
2
Embed Size (px)
DESCRIPTION
Conhecendo um pouco mais sobre a ferramenta para modelagem, simulação e verificação de sistemas em tempo real, UPPAAL.
Citation preview
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