Utilização de Técnicas de Verificação Formal para a Coordenação de Sistemas Multi-Robôs

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

Modelagem

Propriedades esperadas

VERIFICAÇÃO

Sim

Não Contra exemplo

Propriedade satisfeita

correções

SISTEMA

descrição operacional

especificações

Conceitos Básicos 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

12

3

Introdução 8/31

Modelagem

var map: matrix:= [[-1, -1, -1, -1, -1],

[-1, 2, 0, 0, -1],

[-1, 0, -1, 1, -1],

[-1, 0, 0, 0, -1],

[-1, -1, -1, -1, -1]]

2

1

Modelagem 9/31

Modelagem

Robot

Controller

Light sensor Encoder

Initialization

Rotating Right

Rotating Left

Moving Forward

start start

light encode encode

rotateRightrotateLeftmForward

Modelagem 10/31

Inicialização

Procura pelo ID dos robôs em cada linha e coluna

Quando um ID é encontrado suas respectivas coordenadas são atualizadas

Quando todos os ID’s são encontrados é enviado um sinal broadcast start!

Modelagem 11/31

Controle

Espera pelo sinal broadcast start?

Pode enviar rotateLeft! E rotateRight! livremente

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.

Modelagem 12/31

Robô

mForward?: Atualiza a

próxima célula e vai para o

lugar Moving

light?: Libera a célula anterior

rotateLeft? ou rotateRight?: Vai para o

lugar Rotating

encode?: Atualiza a orientação do robô

Modelagem 13/31

Sensores

Light sensor: envia light! Encoder: envia encode!

Modelagem 14/31

Geração de Trace

Verificação de fórmulas de alcançabilidade e a geração de contra-exemplos (shortest trace)

Filtragem das transições sincronizadas entre controlador e robôs

Implementação 15/31

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 }

Arquitetura

Robot

Trace executor

Motors

Environment

Trace generator Trace

Execution confirmation

Instructions

Commands

Information

Sensors

Sensors

Information

Operational control

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

Obstáculos

Trace calculado

Posição inicial

Posição final

Orientação inicial

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

1

2

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

1

2

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

1 2

ROBOT 1 ROBOT 201. TurnL02. TurnL03. GoF04. GoF

05. GoF06. GoF07. TurnR08. GoF09. TurnL10. TurnL11. GoF12. GoF13. GoF14. TurnL15. TurnL16. GoF17. TurnL18. 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

Obrigado!

Victor Boeing Ribeiroboeing@das.ufsc.br