Upload
mateus-chaves-lemos
View
227
Download
2
Embed Size (px)
Citation preview
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.