Programação de veículos autônomos com linguagem BZR (Parte 1)

O Heptagon é um software para a modelagem de sistemas de eventos discretos (SEDs) que utiliza a linguagem BZR para a verificação das propriedades dos SEDs e síntese de controladores para SEDs. Neste post apresentaremos em duas partes o desenvolvimento de um veículo autônomo utilizando o Heptagon/BZR, sintetizando automaticamente o controlador e integrando o código gerado ao Arduino.

Essa proposta envolve uma importante teoria para os SEDs: a teoria de controle supervisório. Nessa teoria assume-se que o veículo (sistema) é composto por um conjunto de sub-sistemas (componentes) e que cada sub-sistema apresenta seu próprio comportamento. Nessa abordagem, um supervisor deve atuar sobre os componentes para garantir o comportamento desejado para o veículo como um todo.

Ao longo do primeiro post, apresentaremos a modelagem dos principais componentes do veículo na linguagem BZR e como sintetizar automaticamente o controlador utilizando o Heptagon. Nesse caso, é importante destacar que é necessário ter o Heptagon/BZR instalado e um tutorial para instalação do Heptagon já foi visto aqui no blog. Por fim, veremos em um segundo post como o código gerado pode ser integrado ao Arduino.

1 Modelagem

O processo de modelagem do veículo consiste em definir o comportamento esperado considerando todas as variáveis de entrada e as ações associadas a essas entradas. Assim, queremos um veículo autônomo que seja capaz de detectar obstáculos e desviar sua rota para evitar a colisão. Isso definido, podemos pensar nos sub-sistemas que compõem o veículo. Consideramos então os sub-sistemas:

• Para que ele possa detectar obstáculos podemos assumir a existência um sensor de distância.
• Necessitaremos também de motores que controlam as rodas do veículo, definindo a direção e sentido.

Definimos então dois sub-sistemas: um sub-sistema que considera o sensor de distância como entrada e que responde se há ou não obstáculo, e outro sub-sistema que define o sentido de giro e velocidade dos motores. Com base nisso, iremos definir as seguintes regras:

1. A distância mínima do veículo para um obstáculo será de 45 cm. Caso a distância seja menor ou igual a 45 cm, ele deverá mudar de direção;
2. O veículo possuirá quatro rodas, logo, quatro motores. Considerando quatro motores, ele poderá mudar a sua direção mudando o sentido do giro de duas dessas rodas: enquanto duas giram para frente, duas giram para trás.

A partir dessas definições, podemos iniciar a modelagem utilizando a linguagem BZR. Nessa abordagem, cada componente deve ser descrito no formalismo de autômatos, usando o conceito de máquinas de estados. Para facilitar a compreensão, os diagramas de cada um dos autômatos acompanham a modelagem de cada sub-sistema.

1.1 Sensor de obstáculos

O autômato que define o sensor de obstáculos pode ser representado por dois estados: há um obstáculo e não há um obstáculo. Assim, podemos assumir que existe uma variável de entrada (dist) que fornece ao sub-sistema o valor da distância entre o veículo e o obstáculo mais próximo. As transições entre os estados acontecem com base nas condições: se a distância é menor ou igual a 45 cm, então há obstáculo. Caso contrário, não há. A resposta do autômato será sempre um valor  associado ao estado atual, verdadeiro (há obstáculo) ou falso (não há obstáculo). Graficamente, podemos representar através da Figura 1.

Com base na Figura 1, podemos implementar o autômato utilizando a linguagem BZR, conforme o código que segue:

Observe que a implementação é extremamente simples e que a informação gerada pode ser interpretada como um sinal. Assim, enquanto o veículo se move, um sinal é sempre atualizado quanto a existência de um obstáculo.

1.2 Motor

Como previsto, a modelagem de quatro motores é necessária para definir o movimento do veículo. Podemos modelar cada um dos motores com um único autômato já que eles terão exatamente o mesmo comportamento.

A modelagem do motor apresenta dois estados possíveis: para frente (FORWARD) ou para trás (BACKWARD). Note que a transição é definida pela variável de entrada c, sendo uma entrada definida pelo controlador que será sintetizado. Essa característica define esse automato como um autômato controlável, diferente do sensor de obstáculos. Dessa forma, as transições entre esses estados poderão ocorrer somente se elas não ferirem as regras definidas. Outras duas variáveis, mode e vel, representam uma constante que define o sentido do giro do motor e a velocidade do giro, respectivamente.

A implementação na linguagem BZR é definida pelo código abaixo.

1.3 Comportamento do veículo

Além desses, um outro autômato deve ser modelado para definir o comportamento do veículo. O autômato Movement também é um automato controlável, logo, as transições dependem da variável c definida pelo controlador para que as regras sejam satisfeitas. O autômato apresenta 3 estados possíveis: MOVING (em movimento), STURNING (iniciar uma rotação) ou TURNING (em rotação). A variável turning define se o veículo está desviando de um obstáculo ou não. Quando o movimento de rotação é iniciado, a variável mbc é incrementada durante doze iterações. Enquanto o mbc for menor que doze, o estado será TURNING. Essa estratégia faz com que o veículo dê uma volta de 120 graus, evitando que ele ainda colida com o obstáculo que o sensor não foi capaz de detectar. Ao retornar para o estado STURNING, a variável mbc assume o valor zero e o veículo pode mover-se para frente ou voltar para o estado TURNING, caso ainda exista obstáculo. A Figura 3 apresenta todos os estados desse autômato.

A implementação em BZR do autômato é apresentado abaixo.

1.4 O controlador

Após definir todos os autômatos, podemos definir o node principal que indicará como os componentes estarão conectados bem como as regras que deverão ser garantidas pelo controlador. Iremos agora definir como cada autômato deverá interagir com o outro para garantir que o veículo tenha o comportamento desejado.

Note que o código abaixo define como entrada o valor da distância obtida pelo sensor (distance). Como variáveis de saída, são esperadas aquelas que definem a existência de um obstáculo (obs), se o veículo está rotacionando (turning), quatro variáveis para definir o estado de cada motor (motor1, …, motor4), quatro variáveis que definem a velocidade de cada motor (vel1, …, vel4) e um contador (mbc).

Observe na linha 6 que as regras 1 e 2 definidas no início da modelagem foram condensadas em uma única regra (rule). Em outras palavras temos: se há obstáculo e o veículo está no estado de rotação (STURNING ou TURNING), então o estado continua definido como TURNING e os motores devem ser ajustados da seguinte forma: motor1 e motor3 giram para frente e motor2 e motor4 giram para trás. O complementar dessa regra diz que: se não houver obstáculo, então todos os motores devem girar para frente e, consequentemente, o veículo deve andar para frente.

Nas linhas 8 e 9 há a declaração enforce com a regra (rule) e a declaração with que indica as variáveis controláveis c_move, c_motor1, c_motor2, c_motor3, c_motor4. O objetivo é fazer com que essas variáveis sejam utilizadas pelo controlador para que a regra seja obedecida. Observe que essas variáveis são argumentos para a chamada dos autômatos entre as linhas 12 e 16. Assim, a partir dessas variáveis, o controlador poderá ajustar o estado de cada autômato para atender a regra.

Por fim, um arquivo nomeado car.ept com todo o código BZR da modelagem deve ser salvo em um diretório exclusivo. O arquivo fica estruturado da seguinte maneira:

2 Sintetizando o controlador

A síntese do controlador propriamente dita depende do Heptagon/BZR e do Sigali, que é capaz de verificar se a lógica das regras está correta, evitando inconsistências e garantindo que o controlador não tenha que lidar com situações de erros em tempo de execução.

Para a síntese, faremos uso do arquivo de Makefile apresentado abaixo para definir as etapas de compilação. Isso permite que a compilação seja feita de modo automático.

As variáveis SIM_PROG, SIM_NODE e CONTRACT_NODE no Makefile definem o nome do arquivo *.ept criado no processo de modelagem, o nome do arquivo para o controlador a ser compilado e o nome do node principal, respectivamente. As linhas 11 e 13 definem o caminho para o Sigali e para o Heptagon, respectivamente. Ao executar o Makefile, o Heptagon deverá gerar arquivos com os formatos *.c e *.z3z, conforme a linha:

A variável $(HEPTC) é definida anteriormente como o heptc, comando para compilar um arquivo de extensão *.ept em C ou Java. No Makefile, definimos a linguagem C passando o c como parâmetro -target. Além disso, geramos o arquivo *.z3z contendo o nome do controlador controller passando como parâmetro a extensão *.z3z. O parâmetro -s indica o nome do node principal, neste caso, controller (o controlador). Por fim, o último parâmetro é o nome do arquivo a ser compilado, o car.ept.

O heptc cria então dois diretórios: car_c (estão os arquivos em *.c) e car_z3z, onde está o arquivo controller.z3z. O arquivo controller.z3z será utilizado como argumento ao Sigali para que a análise das regras seja feita, confome a linha 54 do Makefile:

Após a compilação do Sigali, será gerado o arquivo controller_controller.ept que, após ser novamente compilado pelo heptc (linha 57 do Makefile), irá gerar (finalmente!) o simulador chamado controller_sim.

Com os arquivos car.ept e Makefile em um mesmo diretório, é necessário executar o comando make no terminal para iniciar a compilação. Após esse processo, o controlador é sintetizado e pode ser testado a partir do executável controller_sim. Caso exista algum erro lógico nas regras definidas o Sigali irá sinalizar e o processo de síntese será interrompido. Considerando que todo o processo ocorreu com sucesso, para executar o controlador basta entrar com o comando abaixo no terminal.

3 Continua…

É isso! O processo de modelagem e síntese do controlador utilizando o Heptagon/BZR foi concluído com sucesso. No próximo post apresentaremos com detalhes os passos necessários para integrar ao Arduino o controlador que geramos neste post.