Utilização de Técnicas de Verificação Formal
para a Coordenação de Sistemas Multi-Robôs
Victor Boeing Ribeiro
27 de outubro de 2011
Sumário
 CONCEITOS BÁSICOS
 INTRODUÇÃO
 MODELAGEM UPPAAL
 IMPLEMENTAÇÃO
 EXPANSÃO DO MÉTODO
 REDUÇÃO DE COMPLEXIDADE
 CONCLUSÃO E PERSPECTIVAS
Sumário
2/31
Sistemas a Eventos Discretos
Processos não são governados pela variação de variáveis contínuas,
mas por eventos – alterações instantâneas, sem estados intermediários
 Um Autômato Finito Determinístico é formalmente definido pela
quíntupla G = (X, Σ, f, x0, Xm), onde:
• X: conjunto finito de estados
•Σ: conjunto de eventos (alfabeto)
• f : X, Σ → X função de transição
• x0: estado inicial
• Xm: conjunto de estados finais (marcados)
Conceitos Básicos
3/31
Autômatos Temporizados
 Autômatos temporizados são uma extensão de máquinas de estados
finitos com variáveis de tempo (timers) e variáveis discretas limitadas
• Guard (condição)
• Update (atualização)
• Sync (canal de sincronização)
Conceitos Básicos
4/31
Verificação
 Uso de técnicas matemáticas para provar que uma propriedade é
satisfeita ou não, procurando por sequências de eventos que possam
violá-la
correções
SISTEMA
descrição
operacional
Não
Modelagem
Contra
exemplo
VERIFICAÇÃO
especificações
Conceitos Básicos
Propriedades
esperadas
Sim
Propriedade
satisfeita
5/31
Objetivos
 Coordenação da atividade de movimentação de múltiplos robôs
dentro de um espaço delimitado e com obstáculos;
• Desenvolvimento de um coordenador que forneça uma lista de
instruções a serem executadas pelos robôs para alcançarem a
posição desejada, evitando obstáculos e sincronizando seus
movimentos com outros robôs
Introdução
6/31
Método
 Modelagem do sistema multi-robôs como sistema a eventos
discretos;
 Verificação intencional de propriedades de alcançabilidade;
 Geração de um contra-exemplo com a lista de instruções a serem
executadas pelos robôs
Introdução
7/31
Especificações
 Múltiplos robôs, área limitada e obstáculos;
 Robôs devem respeitar os limites do cenário,
evitar colisões com obstáculos e entre eles;
 Área de trabalho dividida em células:
• Células podem estar livres, ocupadas por
um robô ou obstáculo
 Robôs podem executar três tipos de
movimentos:
• Rotação 90o para direita e esquerda
• Movimento para frente
Introdução
8/31
Modelagem
var map: matrix:= [[-1, -1, -1, -1,
[-1,
2,
[-1,
0,
[-1,
0,
0,
0,
-1, 1,
0,
-1],
-1],
0, -1],
[-1, -1, -1, -1,
Modelagem
-1],
-1]]
9/31
Modelagem
start
start
Initialization
Robot
Controller
rotateRight
rotateLeft
mForward
Moving
Forward
light
Light
sensor
Modelagem
Rotating
Left
encode
Rotating
Right
encode
Encoder
10/31
Inicialização
Quando todos os ID’s são encontrados
é enviado um sinal broadcast start!
Procura pelo ID dos robôs em
cada linha e coluna
Modelagem
Quando um ID é encontrado suas
respectivas coordenadas são atualizadas
11/31
Controle
Espera pelo sinal broadcast start?
Antes de enviar mForward!
o Controlador verifica se a
próxima célula está livre e
se o robô não sairá do
cenário.
Pode enviar rotateLeft! E
rotateRight! livremente
Modelagem
12/31
Robô
encode?: Atualiza a
orientação do robô
light?: Libera a célula
anterior
mForward?:
Atualiza a
próxima célula
e vai para o
lugar Moving
rotateLeft? ou
rotateRight?: Vai para o
lugar Rotating
Modelagem
13/31
Sensores
Light sensor: envia light!
Modelagem
Encoder: envia encode!
14/31
Geração de Trace
 Verificação de fórmulas de alcançabilidade e a geração de contraexemplos (shortest trace)
 Filtragem das transições sincronizadas entre controlador e robôs
 FÓRMULA:
A[] not (x[0]==2 and y[0]==3)
Control.Idle->Control.Idle { 1, rotateLeft[0]!, 1}
Control.Idle->Control.Idle { 1, rotateLeft[0]!, 1}
Control.Idle->Control.Idle { 1, mForward[0]!, 1}
Control.Idle->Control.Idle { 1, rotateRight[0]!, 1}
Control.Idle->Control.Idle { 1, mForward[0]!, 1 }
Implementação
15/31
Arquitetura
Trace generator
Trace
Trace executor
Execution
confirmation
Instructions
Sensors
Information
Operational control
Environment
Information
Commands
Sensors
Motors
Robot
Implementação
16/31
Implementação
Interface para entrada de valores para posição inicial do robô,
orientação e obstáculos
• Essa informação é gravada no arquivo “xml” que contém o
modelo do sistema
Posição objetivo do robô
•Gravada no arquivo “q” que contem a fórmula a ser verificada
 Acesso ao verificador para cálculo do menor contra-exemplo
Envio do trace calculado através de serial Bluetooth
Implementação
17/31
Implementação
Posição inicial
Obstáculos
Posição final
Orientação inicial
Trace calculado
Implementação
18/31
Expansão do método - Objetivos
 Modelagem do sistema com a linguagem FIACRE
 Avaliação da possibilidade de execução de ações simultaneamente,
por diferentes robôs – aumento da eficiência do sistema
 Avaliação da complexidade dos modelos gerados
 Proposta de um método para redução da complexidade
Expansão do Método
19/31
Modelo Sequencial
 Portas TurnR, TurnL e GoF
 Controle responsável por gerenciar a matriz
 Passagem instantânea entre células
Expansão do Método
20/31
Modelo Sequencial
ROBÔ 1
ROBÔ 2
01.
GoF
02.
TurnR
03.
GoF
04.
GoF
05.
GoF
06.
TurnR
07.
GoF
08.
TurnL
09.
TurnL
10.
TurnL
11.
TurnL
12.
GoF
13.
GoF
14.
GoF
15.
TurnL
16.
TurnL
Expansão do Método
21/31
Modelo Paralelo
 Portas TurnR, TurnL, GoF, Release e Wait
 Estado intermediário de movimentação
Instruções enviadas alternadamente para os robôs
Expansão do Método
22/31
Modelo Paralelo
ROBÔ 1
ROBÔ 2
01.
GoF
GoF
02.
Wait
TurnR
03.
Wait
GoF
04.
GoF
TurnL
05.
TurnR
TurnL
06.
GoF
Wait
07.
TurnL
GoF
08.
TurnL
GoF
09.
Wait
GoF
10.
Wait
TurnL
11.
Wait
TurnL
Expansão do Método
23/31
Complexidade
Número de estados
Modelo paralelo
Modelo sequencial
ROBOTS
ROBOTS
CELLS
2
3
2
3
16
168 448
44 311 488
3 840
215 040
25
486 640
231 806 080
9 600
883 200
Expansão do Método
24/31
Método para redução de complexidade
 Desenvolvimento de um método com baixa complexidade e que
mantenha o paralelismo no trace gerado
• Cálculo de um trace sequencial através do modelo de baixa
complexidade
• Algoritmo que avalia quais instruções podem ser executadas
simultaneamente
Redução de complexidade
25/31
Método para redução de complexidade
Redução de complexidade
26/31
Método para redução de complexidade
ROBOT 1
01.
02.
03.
04.
TurnL
TurnL
GoF
GoF
05.
06.
07.
08.
09.
10.
11.
12.
13.
14.
15.
16.
17.
18.
ROBOT 2
GoF
GoF
TurnR
GoF
TurnL
TurnL
GoF
GoF
GoF
TurnL
TurnL
GoF
TurnL
GoF
Redução de complexidade
27/31
Método para redução de complexidade
Redução de complexidade
28/31
Método para redução de complexidade
Redução de complexidade
29/31
Conclusão
 Aumentando a eficiência na geração do trace aumenta-se também o
grau de complexidade do modelo
 Modelo que gera trace com paralelismo não é flexível
e é
impraticável sua aplicação para sistemas com elevado número de robôs
ou células
 Método para redução de complexidade apresentou um bom
resultado, gerando um trace com paralelismo e com um grau de
complexidade muito menor
Conclusão e Perspectivas
30/31
Perspectivas
 Utilização de obstáculos dinâmicos no sistema – portas
 Abordagem através da Teoria de Controle Supervisório
 Abordagem através de Autômatos Jogos Temporizados
Conclusão e Perspectivas
31/31
Victor Boeing Ribeiro
[email protected]
Obrigado!