Especificação de Sistemas de Tempo
Real com Gramática de Grafos
Leonardo Michelon
Simone Costa
Leila Ribeiro
Roteiro
Introdução
Gramática de Grafos Baseada em Objetos (GGBO)
GGBO Temporizada
Semântica de GGBO Temporizada
Verificação de Propriedades
Observações Finais
Abordagem Lógica para GG
2
Introdução
Propõe-se uma abordagem formal para
especificar e analisar sistemas de tempo real;
Uma extensão de Gramática de Grafos Baseada em
Objetos - GGBO;
Semântica é definida em termos de Autômatos
Temporizados ⇒ Verificação Automática de
Propriedades.
3
Introdução
A proposta:
4
–
Provê uma representação compreensiva da estrutura de
dados de um sistema e de sua distribuição (modelo
baseado em objetos);
–
Permite representar situações complexas num nível
intuitivo (layout gráfico).
–
Baseada em conceitos úteis para modelagem em tempo
real (relógios, restrições de tempo);
–
Linguagem de especificação formal (semântica formal);
–
Diretamente verificado com Model Checking.
Roteiro
Introdução
Gramática de Grafos Baseada em Objetos (GGBO)
GGBO Temporizada
Semântica de GGBO Temporizada
Verificação de Propriedades
Observações Finais
Abordagem Lógica para GG
5
Gramática de Grafos Baseada em
Objetos (GGBO)
Sistema baseado em objetos:
–
–
–
Composto de vários objetos. Um objeto não pode ler ou
modificar atributos de outros objetos.
Objetos são instâncias de classes.
Objetos são entidades autônomas que se comunicam de
forma assíncrona via troca de mensagens.
par1
Classe
atr1
Mensagem
par1
Classe
Mensagem
atr2:TAD
par2
Atributos
par2
atr1
6
atr2
TAD
TAD
Gramática de Grafos Baseada em
Objetos (GGBO)
Formada por:
7
Gramática de Grafos Baseada em
Objetos (GGBO)
Formada por:
• um grafo tipo informando
- todos os atributos de todos os tipos de objetos;
- mensagens enviadas/recebidas por cada tipo
de objeto.
8
Gramática de Grafos Baseada em
Objetos (GGBO)
Formada por:
• um grafo inicial especificando
- valores iniciais dos atributos dos objetos;
- mensagens a serem enviadas quando os
objetos são criados.
9
Gramática de Grafos Baseada em
Objetos (GGBO)
Formada por:
• um conjunto de regras especificando
- o comportamento dos objetos quando
recebem mensagens.
10
GGBO
Uma regra é formada por:
um lado esquerdo finito L (condições de ativação):
–
–
–
uma mensagem de ativação;
(somente) atributos do objeto destino da mensagem de
ativação devem aparecer;
valores de tipos abstratos de dados podem ser variáveis.
um lado direito finito R (itens presentes após a
aplicação da regra):
–
11
–
objetos e atributos de L e novos objetos (valores de
atributos podem mudar mas atributos não podem ser
criados nem deletados);
mensagens para objetos de R.
Gramática de Grafos Baseada em
Objetos (GGBO)
Uma aplicação de regra r: L → R especifica uma mudança no
estado do sistema:
–
todos os itens de L devem estar presentes no estado corrente;
–
itens de L mapeados para R (através do morfismo r) devem ser
preservados;
–
itens de L que não tem imagem em R devem ser removidos do
estado corrente;
–
itens de R que não tem pré-imagem em L devem ser criados.
Regras podem ser aplicadas em paralelo (se não há conflito) .
Regras em conflito são escolhidas não-deterministicamente.
12
Gramática de Grafos Baseada em
Objetos (GGBO) – Aplicação de Regra
13
Roteiro
Introdução
Gramática de Grafos Baseada em Objetos (GGBO)
GGBO Temporizada
Semântica de GGBO Temporizada
Verificação de Propriedades
Observações Finais
Abordagem Lógica para GG
14
GGBO Temporizada
Adiciona marca de tempo nas mensagens:
<tmin, tmax>, tmin ≤ tmax.
Tempo relativo: número mínimo/máximo de unidades de
tempo, relativo ao tempo corrente (ct) em que a
mensagem deve ser manipulada.
As possíveis marcas de tempo são:
15
[tmin + ct, tmax + ct]
[t + ct, t + ct]
[0 + ct, tmax + ct]
[0 + ct, +∞)
[tmin + ct, +∞)
[ct, ct]
GGBO Temporizada
Análoga a GGBO, considerando:
–
grafos temporizados: cada mensagem tem um tempo mínimo
/máximo definido (por funções parciais);
–
regras temporizadas: regras com tmin e tmax indefinidos em L.
Regras especificam como manipular uma mensagem, e
não quando elas devem ser entregues.
16
GGBO Temporizada – Exemplo
Sistema Ferroviário Simples
Grafo Tipo
17
GGBO Temporizada – Exemplo
Sistema Ferroviário Simples
Grafo Inicial
18
GGBO Temporizada – Exemplo
Sistema Ferroviário Simples
Regras do Trem
19
GGBO Temporizada – Exemplo
Sistema Ferroviário Simples
Regras do Segmento de Ferrovia / Regras do Portão
20
Roteiro
Introdução
Gramática de Grafos Baseada em Objetos (GGBO)
GGBO Temporizada
Semântica de GGBO Temporizada
Verificação de Propriedades
Observações Finais
Abordagem Lógica para GG
21
Semântica de GGBOs
Sistema de Transição Rotulado:
–
Estados são grafos alcançáveis.
–
Estado inicial é o grafo inicial.
–
Transições descrevem as possíveis aplicações
de regras.
–
Rótulos são os nomes das regras aplicadas.
Não considera nenhuma restrição de
tempo.
22
Semântica de GGBO Temporizada
Tradução para Autômatos Temporizados que estendem os
autômatos usuais adicionando:
23
–
Restrições de relógio aos estados: quantas unidades de tempo
o sistema deve permanecer no estado.
–
Restrições de relógio às transições: sua condição de ativação.
–
Um conjunto (possivelmente vazio) de relógios às transições:
relógios que são zerados com a ocorrência das transições.
Tradução para Autômatos Temporizados
Estados são grafos de GGBOs temporizadas com um relógio
designado para cada mensagem temporizada
–
–
relógios são inicializados com zero
relógios avançam simultaneamente
Restrições de relógio nos estados garantem que o sistema irá
respeitar os limites de tempo máximo.
Transições descrevem possíveis aplicações de regras
–
–
restrições de relógio nas transições garantem que o sistema irá
respeitar os limites de tempo mínimos (se uma mensagem não tem um
tempo limite para ser manipulada, ela pode ser processada em qualquer
tempo)
relógios zerados com as transições são utilizados nas mensagens
temporizadas criadas.
Um autômato temporizado pode ser definido para gramáticas que
24
atingem estados com um número arbitrário (finito) de mensagens.
Tradução para Autômato Temporizado
Aplicações de regras obtêm os estados do autômato.
–
25
não existem restricoes de tempo quando a regra é aplicável
(tmin e tmax são indefinidos)
Tradução para Autômato
Temporizado - Exemplo
26
Tradução para Autômato
Temporizado - Exemplo
O autômato temporizado
completo para este exemplo
tem 36 estados e 40 transições.
27
Roteiro
Introdução
Gramática de Grafos Baseada em Objetos (GGBO)
GGBO Temporizada
Semântica de GGBO Temporizada
Verificação de Propriedades
Observações Finais
Abordagem Lógica para GG
28
Verificação de Propriedades
Ferramenta de Verificação: Uppaal
–
–
Linguagem de Entrada: Autômatos Temporizados
Linguagem de Especificação: CTL
Fórmulas checadas:
29
Verificação de Propriedades
Propriedades Verificadas
30
–
Propriedades de Segurança: ausência de deadlock
(satisfeita). A[] not deadlock.
–
Propriedades de Alcançabilidade: existência de um
caminho onde G7 é alcançável e clock2 tem um valor
menor do que 10 unidades de tempo (não satisfeita). E <>
TA.G7 and clock2<10
–
Propriedades de Continuidade (liveness): verificar se G13
ocorre então G16 ocorrerá. I.e, se um trem viaja para um
segmento de trem que tem um portão, então o portão irá
eventualmente abrir e o trem irá entrar no segmento
(satisfeita). TA.G13
TA.G16
Roteiro
Introdução
Gramática de Grafos Baseada em Objetos (GGBO)
GGBO Temporizada
Semântica de GGBO Temporizada
Verificação de Propriedades
Observações Finais
Abordagem Lógica para GG
31
Observações Finais
GGBO Temporizada estende GGBO para permitir a
especificação e análise de sistemas de tempo real.
Semântica de GGBO Temporizada foi definida em
termos de Autômatos Temporizados ⇒
verificação através de Uppaal.
Trabalhos Futuros:
32
–
Definição de uma semântica para TGGBO sem a tradução
para autômatos temporizados.
–
Prova de propriedades para sistemas com um espaço de
estados infinito.
Roteiro
Introdução
Gramática de Grafos Baseada em Objetos (GGBO)
GGBO Temporizada
Semântica de GGBO Temporizada
Verificação de Propriedades
Observações Finais
Abordagem Lógica para GG
33
Abordagem Lógica para GGs
Motivação
Prova de propriedades de sistemas
especificados em GGs;
Limitação dos verificadores de modelos.
Objetivo: propor uma abordagem lógica para
GGs que permite a prova de propriedades
através da técnica de indução matemática.
34
Abordagem Utilizada
Gramática de Grafos – Estrutura Relacional.
Aplicação de Regra – MS-Transduction.
Abordagem inspirada no trabalho de
Bruno Courcelle.
35
Verificação de Propriedades
Técnica: indução matemática
Tipo de Dado: grafo alcançável
Definindo Operações Recursivas Primitivas (totais)
é possível semi-automatizar a prova por indução:
–
–
36
Base: propriedade vale para G0;
Passo: propriedade vale para cada uma das regras aplicáveis
a um grafo alcançável.
Referências
Michelon, L.; Costa, Simone.; Ribeiro, L. (2006).
Specification of Real-Time Systems with Graph
Grammars. In: XVII Simpósio Brasileiro de
Engenharia de Software (SBES’2006), FlorianópolisSC.
Michelon, L.; Ribeiro, L. Gramática de Grafos Baseada
em Objetos com Tempo. Dissertação de Mestrado,
PPGC - UFRGS.
37