UPPAAL
Model Checker
Overview
by Valerio Rosset
Uppaal

Uppaal é :
–

Uma ferramenta (Toolbox) para verificação formal
de sistemas de tempo real …
Desenvolvido:
–
–
–
UPPsala University (Sweden )
AALborg University (Denmark)
Primeira versão : 1995
Sistemas de Tempo Real
–
–
Sistema de Tempo Real : a correcção dos protocolos e
algoritmos não depende apenas execução ordenada das
acções mas também o tempo em que são realizadas.
Ex: Air Bag, Drive-By-Wire, ABS … etc …
Model Checking
–
–
Modelo A : conjunto de autómatos temporizados
Requisitos F : Definição de propriedades como:


Safety : Coisas ruins nunca acontecem
Liveness: Alguma coisa boa eventualmente acontece
Arquitetura do Uppaal
Ferramenta Uppaal

Interface de Modelação
Ferramenta Uppaal

Interface de Simulação
Ferramenta Uppaal

Interface de Verificação
Modelagem

Locations:
–

Normal, Initial, Urgent and Committed (ações atómicas)
Edges (guards, sincronizadores, updates)
Modelagem

As transições podem ser controladas por :
–
Guards: são expressões lógicas que determinam
as condições para que uma transição ocorra.
–
Sincronizadores: são chamados de channels e
sincronizam ações entre os autómatos do
modelo.
–
Tempo: Invariantes ou Aleatoriamente.
Exemplo 1: Lâmpada



A lâmpada pode ficar em 3 estados
possíveis: desligada, baixa luminosidade,
com alta luminosidade.
O Utilizador pressiona um botão
aleatoriamente para ligar e desligar a
lâmpada.
A transição de baixa luminosidade para alta
se dá com a velocidade com que se
pressiona o botão ( 2 clicks rápidos = Alta).
Exemplo 1: Lâmpada

Autómato Lampada
Exemplo 1: Lâmpada

Autómato Utilizador
Tempo No Uppaal

Uppaal utiliza um modelo de tempo contínuo
–
Clocks (relógios): podem ser declarados de
maneira global ou individualmente aos
autómatos, porém sempre evoluem
sincronicamente.
Tempo no Uppaal
Tempo no Uppaal
Tempo no Uppaal
Tempo no Uppaal
Simulação no Uppaal

Simulando o Exemplo da Lâmpada
Verificando o Modelo

Propriedades (requisitos) são expressas e
definidas utilizando uma simplificação da
linguagem CLT (Computation Tree Logic).
–

Propriedade = State Formulae & Path Formulae
State Formulae : é uma expressão que
identifica um estado no sistema. Ex: i==1 ou
(i==1 and y==1).
Propriedades


Path Formulae: Definem que tipo de
propriedade se quer verificar.
Reachability: Dado um estado P, existe um
caminho onde P é eventualmente satisfeito.
–
E <> P
Propriedades

Safety : “Coisas ruins nunca ocorrem”. Dado
um estado P, o mesmo precisa ser sempre
satisfeito em todos os caminhos.
–
A[] P
Propriedades

Liveness : “Alguma coisa eventualmente
acontece”. Dado um estado P, o mesmo é
eventualmente satisfeito em todos os
caminhos.
–
A <> P
Verificando

Verificando Exemplo 2
–
A[] Obs.taken imply x>=2

–
X é zerado sempre quando x<=2
E<> Obs.idle and x>3

Verifica se existe algum caminho onde X >3
Verificando

Verificando Exemplo 2
–
A[] Obs.taken imply (x>=2 and x<=3)

–
X é zerado sempre entre 2 e 3
A[] Obs.idle imply x<=3

X nunca ultrapassa o limite
Facilidades

Uppaal ainda permite a utilização de
diversas estruturas como arrays bem como a
possibilidade de implementar funções e
procedimentos onde é executar cálculos e
verificações mais complexas (Sintaxe C++).

Simulação e geração de Traces permite
permite um fast debugging do modelo.
Obrigado !!!!

For More : www.uppaal.org