Checagem de arquiteturas de controle de veículos submarinos: uma abordagem baseada em... por Fábio Henrique de Assis - Versão HTML
Faça o download do livro em PDF, ePub, Kindle para obter uma versão completa.
Fábio Henrique de Assis
Checagem de Arquiteturas de Controle de
Veículos Submarinos: uma abordagem
baseada em especificações formais
Dissertação apresentada à Escola Poli-
técnica da Universidade de São Paulo
para obtenção de Título de Mestre em
Engenharia.
São Paulo
2009
Fábio Henrique de Assis
Checagem de Arquiteturas de Controle de
Veículos Submarinos: uma abordagem
baseada em especificações formais
Dissertação apresentada à Escola Poli-
técnica da Universidade de São Paulo
para obtenção de Título de Mestre em
Engenharia.
Área de concentração:
Controle e Automação
orientador: Newton Maruyama
São Paulo
2009
Este exemplar foi revisado e alterado em relação à versão original, sob
responsabilidade única do autor e com a anuência de seu orientador.
São Paulo, de julho de 2009.
Assinatura do autor _____________________________________
Assinatura do orientador_________________________________
FICHA CATALOGRÁFICA
Assis, Fábio Henrique de
Checagem de arquiteturas de controle de veículos submari-
nos: uma abordagem baseada em especificações formais / F.H.
de Assis. -- ed.rev. -- São Paulo, 2009.
144 p.
Dissertação (Mestrado) - Escola Politécnica da Universidade
de São Paulo. Departamento de Engenharia Mecatrônica e de
Sistemas Mecânicos.
1. Submersíveis não tripulados 2. Arquitetura de software
(Especificação) I. Universidade de São Paulo. Escola Politécnica.
Departamento de Engenharia Mecatrônica e de Sistemas Mecâ –
nicos. II. t.
Dedicatória
à minha família.
Agradecimentos
Gostaria de agradecer primeiramente aos meus pais e ao meu irmão, que
sempre me apoiaram em todas as escolhas que tomei em relação à minha carreira,
principalmente nos momentos mais difíceis.
Agradeço também à minha namorada por estar sempre comigo, e muitas
vezes por compreender minhas ausências que se fizeram necessárias ao longo deste
trabalho.
Não poderiam ficar de fora as pessoas que contribuíram de maneira efetiva
para que esse trabalho fosse concluído, que são meu orientador e meus colegas
de laboratório, além de todos os membros da XMobots, opinando, discutindo e
muitas vezes ajudando a desenvolver certas partes do trabalho.
"O único lugar onde sucesso vem antes do trabalho é no dicionário"
Albert Einstein
Resumo
O desenvolvimento de arquiteturas de controle para veículos submarinos é
uma tarefa complexa. Estas podem ser caracterizadas pelos seguintes atribu-
tos: tempo real, multitarefa, concorrência e comunicações distribuídas em rede.
Neste cenário, existem múltiplos processos sendo executados em paralelo, possi-
velmente distribuídos, e se comunicando uns com os outros. Neste contexto, o
modelo comportamental pode levar a fenômenos como deadlocks, livelocks, dis-
puta por recursos, entre outros. A fim de se tentar minimizar os efeitos de tais
dificuldades, neste trabalho será apresentado um método para checagem de mode-
los de arquiteturas de controle de veículos submarinos baseado em Especificações
Formais. A linguagem de especificação formal escolhida foi CSP-OZ, uma com-
binação de CSP e Object-Z. Object-Z é uma extensão orientada a objetos da
linguagem Z para a especificação de predicados, tipicamente pré e pós condições,
além de invariantes de dados. CSP ( Communicating Sequential Process) é uma
álgebra de processos desenvolvida para descrever modelos comportamentais de
processos paralelos. A checagem de modelos especificados formalmente consiste
na análise das especificações para verificar se um sistema possui certas propri-
edades através de uma busca exaustiva em todos os estados em que este pode
entrar durante sua execução. Neste contexto, é possível checar corretude, live-
locks, deadlocks, etc. Além disso, pode-se relacionar duas especificações diferentes
a fim de se checar relações de refinamento. Para as especificações, o verificador
de modelos FDR da Formal Systems Ltd. será utilizado. A implementação é
desenvolvida utilizando um perfil da linguagem Ada denominado RavenSPARK,
uma junção do perfil Ravenscar (desenvolvido na Universidade de York) com a
linguagem SPARK (um subconjunto da linguagem Ada desenvolvido pela Praxis,
Inc.). O Ravenscar é um perfil para desenvolvimento de processos, e portanto os
processos de CSP, incluindo seus canais de comunicação, podem ser facilmente
criados. Por outro lado, SPARK é uma linguagem onde podem ser inseridos
predicados para os dados (originalmente especificados em Object-Z) utilizando
anotações da própria linguagem. A linguagem SPARK possui uma ferramenta,
o Examinador, que pode checar códigos de modelos baseado nestas anotações.
Em resumo, o método proposto permite tanto a checagem de modelos em CSP
quanto a checagem no nível de código. Para isso, as especificações em Object-Z
devem inicialmente ser convertidas em um código na linguagem SPARK junta-
mente com suas respectivas anotações, para que então a checagem do modelo
possa ser realizada no código. O desenvolvimento de uma arquitetura de controle
reativa para um ROV denominado VSOR (Veículo Submarino Operado Remota-
mente) é utilizado como exemplo de uso do método proposto. Toda a arquitetura
de controle é codificada utilizando a linguagem Ada com o perfil RavenSPARK
e embarcada em um computador do tipo PC104 com o sistema operacional de
tempo real VxWorks, da Windriver, Inc.
Abstract
The development of control architectures for Underwater Vehicles is a com-
plex task. These control architectures might be chracterised by the following
attributes: real-time, multitasking, concurrency, and distributed over communi-
cation networks. In this scenario, we have multiple processes running in parallel,
possibly distributed, and engaging in communication between each other. In this
context, the behavioural model might lead to phenomena like deadlocks, live-
locks, race conditions, among others. In order to try to minimize the effects of
such difficulties, in this work a method for model checking control architectures
of underwater vehicles based on formal specifications is presented. The chosen
formal specification language is CSP-OZ, a combination of CSP and Object-Z.
Object-Z is an object-oriented extension of Z for the specification of predicates,
typically, data pre, post and invariant conditions. CSP (Communicating Sequen-
tial Process) is a process algebra developed to describe behavioural models of
parallel process. The model checking of formal specifications is a task of rea-
soning on specifications in which a system verifies certain properties by means
of an exhaustive search of all possible states that a system could enter during
its execution. In this context, it is possible to check about correctness, liveness,
deadlock, etc. Also, one can relate two different specifications in order to check
a refinement ordering. For the specifications, the model checker FDR of Formal
Systems Ltd. is utilised. The implementation is developed using an ADA lan-
guage profile called RavenSPARK, a union of the Ravenscar profile (developed at
the University of York) and the SPARK language (a subset of the ADA language
developed by Praxis, Inc.). The Ravenscar is a profile for developing processes,
so CSP processes including their message channels can be easily deployed. On
the other hand, SPARK is a language where one can insert data predicates (ori-
ginally specified in Object-Z) using language annotations. The SPARK language
has a tool, the Examiner, that can model check code based on these annotations.
In summary, the proposed method allows model checking of CSP processes but
does not allow any checking in the code level. On the contrary, Object-Z spe-
cifications must first be converted into a SPARK language code, together with
proper annotations, and then model checking can be realised in code. The de-
velopment of a real-time reactive control architecture of an ROV named VSOR
(Veiculo Submarino Operado Remotamente) is used as an example of the use of
the proposed method. The whole control architecture is coded using the ADA
Language with the RavenSPARK profile and deployed into a PC104 cpu system
running the Vxworks real-time operating system of Windriver, Inc.
Lista de Figuras
1.1 Exemplos de Veículos Não-Tripulados. . . . . . . . . . . . . . . p. 16
1.2 Desempenho entre os diferentes métodos de verificação de mo-
delos (BRAT et al., 2003). . . . . . . . . . . . . . . . . . . . . . . p. 19
1.3 Esquema do Método Proposto. . . . . . . . . . . . . . . . . . . . p. 21
2.1 Máquina de estados da especificação CSP do processo P. . . . . p. 30
2.2 Esquema de funcionamento do paradigma Híbrido. . . . . . . . p. 34
3.1 Método de Desenvolvimento Proposto. . . . . . . . . . . . . . . p. 37
3.2 Exemplo de Especificação em gCSP. . . . . . . . . . . . . . . . . p. 40
3.3 Modelo Produtor / Consumidor em gCSP. . . . . . . . . . . . . p. 50
3.4 Verificação do modelo Produtor - Consumidor no FDR. . . . . . p. 53
3.5 Execução do modelo Produtor / Consumidor no VxWorks. . . . p. 62
4.1 Esquema de monitoramento com ROVs. . . . . . . . . . . . . . . p. 64
4.2 Robô utilizado no trabalho. . . . . . . . . . . . . . . . . . . . . p. 67
4.3 Interface gráfica de controle do ROV. . . . . . . . . . . . . . . . p. 69
4.4 Comandos de atuação do ROV. . . . . . . . . . . . . . . . . . . p. 70
4.5 Módulos de Software presentes no Sistema. . . . . . . . . . . . . p. 71
4.6 Casos de Uso dos Módulos de Software do Sistema. . . . . . . . p. 72
5.1 Arquitetura de Software - Canais e Estruturas de Dados. . . . . p. 75
6.1 Análise da Arquitetura no FDR. . . . . . . . . . . . . . . . . . . p. 99
6.2 Execução da Arquitetura de Controle no VxWorks. . . . . . . . p. 104
Lista de Tabelas
4.1 Conjunto de sensores embarcados no ROV. . . . . . . . . . . . . p. 67
4.2 Semântica de Comunicação. . . . . . . . . . . . . . . . . . . . . p. 71
6.1 Tempo de Análise da Arquitetura no FDR. . . . . . . . . . . . . p. 99
Sumário
1 Introdução
p. 15
1.1 Objetivos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 20
1.2 Uma breve apresentação do método proposto . . . . . . . . . . . p. 20
1.3 Contribuições . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 23
1.4 Organização do Trabalho . . . . . . . . . . . . . . . . . . . . . . p. 24
2 Conceitos Básicos
p. 25
2.1 Modelagem de Software . . . . . . . . . . . . . . . . . . . . . . p. 25
2.2 UML-RT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 25
2.3 Métodos Formais . . . . . . . . . . . . . . . . . . . . . . . . . . p. 27
2.3.1
CSP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 29
2.3.2
Object-Z . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 30
2.3.3
CSP-OZ . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 32
2.4 Arquiteturas de Controle . . . . . . . . . . . . . . . . . . . . . . p. 33
2.5 Conclusões do Capítulo . . . . . . . . . . . . . . . . . . . . . . . p. 36
3 Método de Desenvolvimento
p. 37
3.1 Modelagem do Sistema . . . . . . . . . . . . . . . . . . . . . . . p. 38
3.1.1
Diagrama de Estrutura em CSP . . . . . . . . . . . . . . p. 38
3.1.2
Especificação dos Componentes em CSP-OZ . . . . . . . p. 40
3.1.3
Checagem do Modelo . . . . . . . . . . . . . . . . . . . . p. 42
3.2 Implementação do Modelo . . . . . . . . . . . . . . . . . . . . . p. 44
3.2.1
Geração de Código . . . . . . . . . . . . . . . . . . . . . p. 45
3.2.2
Anotações SPARK . . . . . . . . . . . . . . . . . . . . . p. 48
3.2.3
Checagem da Implementação . . . . . . . . . . . . . . . p. 49
3.3 Testes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 49
3.4 Exemplo de Aplicação: modelo Produtor/Consumidor . . . . . . p. 50
3.4.1
Modelagem . . . . . . . . . . . . . . . . . . . . . . . . . p. 50
3.4.2
Implementação . . . . . . . . . . . . . . . . . . . . . . . p. 54
3.4.3
Testes . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 61
3.5 Conclusões do Capítulo . . . . . . . . . . . . . . . . . . . . . . . p. 61
4 Sistema para Controle de ROVs
p. 63
4.1 Descrição Geral . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 63
4.2 Requisitos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 64
4.2.1
Modos de Operação . . . . . . . . . . . . . . . . . . . . . p. 64
4.2.2
Modos de Movimentação . . . . . . . . . . . . . . . . . . p. 65
4.2.3
Requisitos de Desempenho . . . . . . . . . . . . . . . . . p. 65
4.2.4
Requisitos Temporais . . . . . . . . . . . . . . . . . . . . p. 66
4.3 Componentes do Sistema . . . . . . . . . . . . . . . . . . . . . . p. 66
4.3.1
O Robô . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 66
4.3.2
Estação Base . . . . . . . . . . . . . . . . . . . . . . . . p. 67
4.4 Arquitetura de Hardware . . . . . . . . . . . . . . . . . . . . . . p. 71
4.5 Conclusões do Capítulo . . . . . . . . . . . . . . . . . . . . . . . p. 73
5 Especificação da Arquitetura do Software Embarcado
p. 74
5.1 Introdução . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 74
5.2 Definições Gerais . . . . . . . . . . . . . . . . . . . . . . . . . . p. 75
5.2.1
Tipos Básicos de Dados . . . . . . . . . . . . . . . . . . p. 75
5.2.2
Estruturas de Dados . . . . . . . . . . . . . . . . . . . . p. 77
5.2.3
Processos Periódicos . . . . . . . . . . . . . . . . . . . . p. 78
5.3 Camada Deliberativa . . . . . . . . . . . . . . . . . . . . . . . . p. 80
5.3.1
BaseReader . . . . . . . . . . . . . . . . . . . . . . . . . p. 81
5.3.2
Remote . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 82
5.3.3
Autonomous . . . . . . . . . . . . . . . . . . . . . . . . . p. 82
5.3.4
S1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 83
5.4 Camada Reativa . . . . . . . . . . . . . . . . . . . . . . . . . . p. 84
5.4.1
Compass . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 85
5.4.2
Altimeter . . . . . . . . . . . . . . . . . . . . . . . . . . p. 86
5.4.3
Sonar . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 87
5.4.4
BaseWriter . . . . . . . . . . . . . . . . . . . . . . . . . p. 88
5.4.5
ThrusterWriter . . . . . . . . . . . . . . . . . . . . . . . p. 89
5.4.6
Move . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 90
5.4.7
S2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 92
5.4.8
Stop . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 92
5.4.9
Sensor . . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 93
5.4.10 AvoidCollision . . . . . . . . . . . . . . . . . . . . . . . . p. 94
5.4.11 Actuator . . . . . . . . . . . . . . . . . . . . . . . . . . . p. 95
5.5 Conclusões do Capítulo . . . . . . . . . . . . . . . . . . . . . . . p. 96
6 Resultados
p. 98
6.1 Verificação do Modelo . . . . . . . . . . . . . . . . . . . . . . . p. 98
6.2 Verificação da Implementação . . . . . . . . . . . . . . . . . . . p. 100
6.3 Testes no Sistema Embarcado . . . . . . . . . . . . . . . . . . . p. 104
7 Conclusões
p. 106
Referências
p. 108
Apêndice A - Notação de Object-Z e CSP
p. 112
A.1 Notação da linguagem Object-Z . . . . . . . . . . . . . . . . . . p. 112
A.2 A notação da linguagem CSP . . . . . . . . . . . . . . . . . . . p. 115
Anexo A - Script CSPM da Arquitetura de Controle
p. 118
Anexo B - Códigos Fonte da Arquitetura de Controle
p. 119
15
1
Introdução
Atualmente, sistemas embarcados estão presentes em equipamentos com os
quais temos contato direto em nosso dia a dia, como aparelhos eletro-eletrônicos,
automóveis, sistemas de controle de temperatura de ambientes, entre outros.
Além destas aplicações mais comuns, eles também são encontrados em sistemas
onde é necessário haver maior confiabilidade e determinismo no comportamento
do sistema. Isso porque uma falha em tais sistemas pode implicar em grandes
prejuízos financeiros ou até mesmo na perda de vidas. Alguns exemplos são os
softwares de controle de trens, aeronaves, plantas de usinas nucleares, entre ou-
tros. Sistemas deste tipo são denominados Sistemas Críticos ou Sistemas de Alta
Integridade 1.
No contexto deste trabalho, os sistemas embarcados são aplicados em robôs
móveis, também conhecidos como Veículos Não-Tripulados. Estes são veículos
capazes de operar em diversos meios como ar (UAVs2), terra (UGVs3.) e água
(AUVs4 e ROVs5). A figura 1.1(a) mostra um exemplo de Veículo Aéreo Não-
Tripulado (VANT), o Apoena, da empresa brasileira XMobots (XMOBOTS, 2009).
Na figura 1.1(b) temos um exemplo de veículo submarino do tipo ROV que apre-
senta garras atuadoras, o Panther Plus, da empresa inglesa Saab Seaeye (SAAB,
2009). E por fim, a figura 1.1(c) mostra o robô terrestre Pioneer 2DX, da em-
presa Mobile Robots (MOBILE, 2009). A característica marcante destes veículos
consiste na sua capacidade de operar sem a presença de um piloto em seu interior.
Existem dois modos básicos de operação: remoto, onde o piloto envia comandos
de atuação para o robô por meio de um canal de comunicação, que pode ser
um cabo, um link de rádio, entre outros; autônomo, onde o veículo opera sem
nenhum tipo de intervenção humana. Dos tipos de veículos mencionados acima,
neste trabalho será utilizado um submarino do tipo ROV, operando em modo
remoto por meio de uma estação de controle.
1em inglês estes sistemas são denominados Safety-Critical ou High Integrity Systems.
2do inglês, Unmanned Aerial Vehicles.
3do inglês, Unmanned Grounded Vehicles
4do inglês, Autonomous Underwater Vehicles.
5do inglês, Remotely Operated Vehicles.
1 Introdução
16
(a) Aéreos
(b) Aquáticos
(c) Terrestres
Figura 1.1: Exemplos de Veículos Não-Tripulados.
Do ponto de vista do software de controle destes veículos, estes podem ser
considerados Sistemas de Tempo Real. Segundo Burns (2001), um sistema de
tempo real é qualquer sistema de processamento de informações que deve respon-
der a estímulos de entrada gerados externamente em um dado período de tempo
finito e previamente especificado. Nestes sistemas, a corretude não depende ape-
nas do resultado lógico, mas também do tempo em que ele foi obtido. Logo, um
atraso na resposta pode ser tão ruim quanto uma resposta errada. Estes podem
ser classificados em quatro categorias quanto sua tolerância à falhas:
Hard Real Time Systems: são sistemas onde é imprescindível que as respos-
tas ocorram dentro dos limites de tempo pré-estabelecidos. Nesse caso, os
erros precisam ser todos rastreados de forma a permitir uma ação imediata
de tratamento dos mesmos. Um exemplo de sistema de tempo real crítico
são os sistemas de controle de vôo;
Soft Real Time Systems: sistemas onde os limites de tempo são importan-
tes, mas que ainda continuam funcionando caso algum destes limites seja
rompido ocasionalmente. Um exemplo disso são sistemas de aquisição de
dados;
Real Real Time Systems: são sistemas que são hard real time e que possuem
tempos de resposta muito curtos. Um exemplo seria um sistema de controle
de mísseis;
Firm Real Time Systems: o sistema de tempo real firme, ou firm real time
é aquele no qual tarefas atrasadas não são aproveitáveis, mas ainda funci-
onam corretamente caso alguns prazos ou processos sejam ocasionalmente
perdidos. Sistemas assim costumam ser utilizados em aplicações multimídia
ou de realidade virtual que requerem características avançadas de sistemas
operacionais.
Dada a classificação acima, a arquitetura de controle desenvolvida neste tra-
1 Introdução
17
balho será considerada um sistema soft real time, uma vez que não serão feitas
provas nem análises quanto a restrições temporais. Entretanto, tais aspectos farão
parte do projeto.
O desenvolvimento de arquiteturas de controle para veículos submarinos é
uma tarefa complexa. Além do fato destas se caracterizarem como sistemas de
tempo real, existem ainda outras características que devem ser mencionadas que
fazem parte de seu projeto, dificultando-o consideravelmente. A principal delas
é a presença de concorrência. Os softwares de controle de robôs móveis frequen-
temente apresentam concorrência, onde o sistema de controle é composto por
diversos processos sendo executados em paralelo, interagindo uns com os outros
e disputando recursos de hardware como regiões de memória compartilhada e
tempo de processamento. O aspecto crucial que torna os sistemas concorrentes
diferentes dos seqüenciais é o fato de seus processos se comunicarem uns com os
outros. O projeto de tais sistemas requer modos de se lidar com a complexidade
inerente destas comunicações. Isso porque a concorrência por si só introduz fenô-
menos que não estão presentes em sistemas sequenciais, como (BELAPURKAR,
2005):
• Deadlock : é a condição onde um processo fica bloqueado indefinidamente
por estar esperando que uma determinada condição se torne verdadeira, tal
como um recurso tornar-se disponível, mas tal condição se tornar verdadeira
depende deste mesmo processo que estava esperando fazer algo. Assim, dois
ou mais processos ficam esperando os outros darem o primeiro passo, sendo
que nenhum é capaz de fazer nada;
• Livelock : quando um programa entra em um loop infinito e não interage
mais com o ambiente, este comportamento é denominado divergência. Sis-
temas paralelos apresentam livelock, que simboliza uma atividade interna
que é executada infinitamente, impedindo que o sistema interaja com o
ambiente. Do ponto de vista de um usuário, um programa em livelock é
similar a um programa em deadlock. Porém, o primeiro pode ser pior, pois
o usuário é capaz de observar alguma atividade interna, e em razão disso
esperar eternamente por uma resposta do sistema(ROSCOE; HOARE; BIRD,
1997).
• Disputa por recursos: diz-se que existe uma disputa por recursos em um
sistema quando existe um recurso compartilhado entre múltiplos processos
e o vencedor determina o comportamento do sistema. Um problema resul-
tante disso, onde a principal causa é a sincronização incorreta de acessos a
1 Introdução
18
um recurso compartilhado, consiste na corrupção dos dados compartilha-
dos, onde um processo faz a leitura do dado antes que um outro termine de
atualizá-lo.
• Starvation: pode ocorrer em sistemas concorrentes em que os processos
possuem prioridade de execução. O fenômeno consiste em um processo de
baixa prioridade nunca ser executado devido à execução dos outros de maior
prioridade.
Estes problemas não surgem a partir do comportamento dos componentes
individuais, e sim através do modo como eles interagem, não aparecendo durante
o desenvolvimento e nos testes individuais dos componentes de um sistema. Uma
teoria de concorrência como o CSP (ROSCOE; HOARE; BIRD, 1997), que será apre-
sentada posteriormente, oferece um modo de controlar tais problemas (SCHNEI-
DER, 1999). Outra característica relevante consiste na dificuldade na depuração
de erros no sistema desenvolvido quando este já está embarcado no robô. Neste
caso, a depuração de eventuais erros é uma tarefa difícil de ser realizada, uma vez
que em geral não existem muitos recursos para se monitorar os estados do sistema
já operando embarcado. Por exemplo, caso haja alguma falha no software que
cause uma parada repentina do veículo, será muito difícil identificar a causa do
problema para que o erro seja consertado.
Como uma tentativa de se minimizar as dificuldades apresentadas anterior-
mente, vêm sendo proposto o uso de métodos formais no desenvolvimento de
software. Estes consistem basicamente no uso de linguagem matemática na espe-
cificação de software, e serão apresentados com maiores detalhes na seção 2.3. Seu
uso é mais comum na área de sistemas críticos, mas também existem aplicações
na indústria. Um exemplo disso é a utilização de métodos formais para especi-
ficação e validação de sistemas de tempo real apresentado por Sherif, Sampaio
e Cavalcante (2001). Esta abordagem foi aplicada na especificação do computa-
dor de bordo do primeiro satélite para aplicações científicas (SACI-I), do Instituto
Nacional de Pesquisas Espaciais - INPE (SHERIF; SAMPAIO; CAVALCANTE, 2003).
Outro exemplo de aplicação de métodos formais na indústria é o trabalho de La-
wrence (2005), onde é mostrada a aplicação de CSP em um sistema desenvolvido
na empresa IBM. Neste caso, a parte especificada formalmente (em CSP) foi pos-
teriormente validada no checador de modelos FDR (SYSTEMS, 2005), e depois
exaustivamente testada tanto pelo fabricante quanto pelo cliente. Após a rea-
lização dos testes não foram encontrados erros, o que mostra a importância da
utilização de especificações formais no desenvolvimento de software.
1 Introdução
19
Apesar de existirem diversas aplicações de especificações formais, a linguagem
de modelagem mais utilizada na indústria é o UML ( Unified Modeling Language)
(OMG, 2004). Esta se tornou um dos padrões para modelagem e projeto de siste-
mas de software mais utilizados devido principalmente a sua notação semi-formal
ser relativamente fácil de se utilizar e ser bem suportada por ferramentas de
desenvolvimento (AKHLAKI et al., 2006). Entretanto, existem diversos trabalhos
que visam formalizar partes da linguagem, como é o caso, por exemplo, dos tra-
balhos de Akhlaki et al. (2006), Yeung et al. (2005) e Ng e Butler (2002), que
utilizam regras de mapeamento de diagramas em UML para gerar especificações
formais em diversas linguagens, como Z (LIGHTFOOT, 1991), OhCircus (BORGES;
MOTA, 2007), CSP-OZ (FISCHER, 1997), entre outras. Uma outra abordagem
desse tipo é a do trabalho de Moller et al. (2008), onde foi proposta uma metodo-
logia utilizando modelagem em UML-RT, geração de especificações em CSP-OZ
e implementação em Java.
No desenvolvimento de arquiteturas de controle de robôs móveis, foram en-
contrados apenas dois trabalhos que utilizam métodos formais. O primeiro deles
é o de Medeiros, Chatila e Fleury (1996), que descreve a especificação de uma
arquitetura de controle para robôs móveis autônomos, sendo verificados a exis-
tência de deadlocks, tempos de reação e detecção de inconsistências. O outro é o
trabalho de Champeau et al. (2000), que utiliza métodos formais e orientação a
objetos no desenvolvimento do software embarcado de AUVs. O objetivo é anali-
sar as possibilidades e limitações de um desenvolvimento conjunto com orientação
a objetos e especificações formais.
Figura 1.2: Desempenho entre os diferentes métodos de verificação de modelos
(BRAT et al., 2003).
A principal vantagem do uso de especificações formais é a possibilidade de
1.1 Objetivos
20
checagem dos modelos antes de sua implementação. O trabalho de Brat et al.
(2003) mostra um estudo experimental para determinar o grau de maturidade de
três diferentes tecnologias de verificação e validação comparadas com o tradicional
teste para encontrar erros em um exemplo representativo, que foi o software de
um robô enviado ao planeta Marte pela NASA, a agência espacial americana. A
figura 1.2 mostra um dos resultados da pesquisa, mostrando a quantidade de erros
( bugs) encontrados com testes (TT), checagem de modelos (MC - Model Checking)
e análise em tempo de execução (RT - Run-Time Analysis), para um total de dez
falhas conhecidas inseridas no sistema. Podemos observar que de todos eles, os
testes foram os menos efetivos na captura de erros no sistema, principalmente os
relacionados aos aspectos de concorrência, que são os deadlocks e as disputas por
recursos ( race conditions). Neste trabalho o método proposto permite que sejam
utilizadas as duas outras técnicas mais efetivas: o Model Checking, feito a partir
do modelo em CSP e a análise em tempo de execução ( Run-Time Analysis),
podendo ser feita tanto com a ajuda da ferramenta da linguagem SPARK que
será apresentada posteriormente ou então na fase de testes, com as ferramentas
do sistema operacional de tempo real VxWorks.
1.1
Objetivos
Este trabalho tem por objetivo principal estabelecer um método para de-
senvolvimento de arquiteturas de controle para veículos submarinos utilizando
especificações formais. O método deve apoiar o desenvolvimento da fase de espe-
cificação do projeto até a geração de código para sistemas embarcados.
1.2
Uma breve apresentação do método proposto
O ponto crucial de um possível método para a verificação formal de sistemas
é a escolha da linguagem de especificação. Neste trabalho, opta-se por CSP-OZ
(FISCHER, 1997). Nesta linguagem, a especificação do modelo pode ser dividida
em duas partes: uma de processos (CSP) e outra de dados (Object-Z). Em CSP-
OZ, ambas as partes estão interconectadas. A parte Object-Z é transformada
em um processo CSP. Desta forma, eventos da parte CSP aparecem como cha-
madas de métodos da parte Object-Z. Pré condições atuam como guardas, i.e.,
evitando ou permitindo a operação específica. Pós-condições definem para qual
estado o processo vai transitar. Uma conseqüência deste esquema é que tanto
o refinamento da parte CSP quanto da parte Object-Z estão unificadas pela se-
1.2 Uma breve apresentação do método proposto
21
mântica de falhas e divergências (FISCHER; WEHRHEIM, 2000). Esta particular
configuração permite que se possa verificar separadamente a parte CSP da parte
Object-Z. Neste trabalho não serão elaboradas pré e pós condições para os méto-
dos, e portanto não serão feitas provas formais. As checagens na implementação
serão feitas com base nos tipos de dados definidos nas especificações.
Deste modo foi proposto um método de desenvolvimento, cujo esquema pode
ser visto na figura 1.3, e que será melhor descrito no capítulo 3. Tal método deve
permitir a especificação dos diversos processos que compõem uma arquitetura
de controle, além de suas estruturas de dados internas e modos de comunicação.
CSP define os processos e seus modos de interação por meio de canais de comu-
nicação síncronos e unidirecionais, e portanto o método proposto deve permitir
a transformação tanto dos processos quanto dos canais de comunicação de CSP
para código de um modo simples.
Figura 1.3: Esquema do Método Proposto.
De acordo com o esquema mostrado na figura 1.3, o desenvolvimento possui
dois focos principais, que são cobertos em etapas separadas. Primeiramente o
modelo é desenvolvido com foco na parte de processos, para posteriormente este
passar para a parte de dados do sistema. Sendo assim, são realizadas duas che-
cagens ao longo do desenvolvimento da arquitetura de controle: uma relacionada
à parte de processos (CSP) e outra à parte de dados (Object-Z).
A primeira das checagens é feita no modelo em CSP com base em um script
gerado automaticamente pela ferramenta gCSP (JOVANOVIC et al., 2004) e poste-
1.2 Uma breve apresentação do método proposto
22
riormente editado manualmente a fim de levar em conta a especificação completa
do sistema em CSP-OZ. A checagem do script é feita com a ferramenta FDR, da
Formal Systems (SYSTEMS, 2005), identificando possíveis erros no modelo como
presença de deadlocks, livelocks e indeterminismos. Assim, após feita a checagem
do modelo, caso este não apresente erros, passa-se à sua implementação. Neste
caso, tanto o código quanto as anotações SPARK (que são usadas na verifica-
ção da implementação) são gerados manualmente com base na parte Object-Z da
especificação em CSP-OZ. Isso permite que seja feita a segunda das checagens
utilizando o examinador da linguagem SPARK, denominado SPARK examiner,
que verifica se as anotações estão de acordo com o código fonte da implementação,
além verificar a existência de erros no fluxo de dados do programa.
Por fim, depois de checados o modelo e sua implementação, o código gerado
pode então ser compilado e testado no VxWorks, onde são realizados os testes
com o código em execução.
Como um exemplo real de aplicação do método proposto, foi desenvolvida
uma arquitetura de controle para um veículo submarino operado remotamente
(ROV), que será futuramente embarcada no robô descrito na seção 4.3.1. Como
será detalhado na seção 2.4, esta foi desenvolvida com base no paradigma híbrido
(MURPHY, 2000), possuindo tanto uma camada deliberativa que inclui as funções
de comando do robô quanto uma camada reativa, onde estão encapsuladas as fun-
ções básicas de funcionamento do robô como leitura de sensores, comunicação e
atuação. Apesar de ter sido colocado na arquitetura com o objetivo de implemen-
tações futuras, o modo autônomo de operação do robô não será implementado, e
portanto o foco deste desenvolvimento se concentrou no modo remoto de opera-
ção. Um ponto importante a se ressaltar é que apesar de terem sido levados em
conta na implementação da arquitetura, os aspectos temporais do sistema não
foram levados em conta nas especificações em CSP-OZ.
De um modo geral, para esta arquitetura foram feitos:
• toda a modelagem do sistema utilizando a linguagem formal CSP-OZ, in-
cluindo a estrutura do sistema com seus diversos processos e canais de
comunicação. Foram especificadas também todos os tipos básicos de dados
e também as estruturas de dados utilizadas pelos processos;
• checagem do modelo em CSP-OZ com o FDR a fim de se verificar presença
de deadlocks, livelocks e determinismo do modelo;
• implementação do modelo em CSP-OZ utilizando a linguagem de progra-
1.3 Contribuições
23
mação SPARK Ada em conjunto com o padrão Ravenscar;
• checagem da implementação por meio do examinador da linguagem SPARK,
a fim de verificar a consistência das anotações com o código fonte, além de
verificar erros no fluxo de dados do programa;
• testes do sistema embarcado em VxWorks.
1.3
Contribuições
As seguintes contribuições são postuladas neste trabalho:
1. Utilização da linguagem CSP-OZ para especificação de arquiteturas de con-
trole de robôs submarinos. Conforme afirmado anteriormente, não existem
muitos trabalhos que utilizam métodos formais na área de robótica. Neste
sentido este trabalho apresenta uma contribuição ao utilizar uma lingua-
gem formal na modelagem do sistema. Esta linguagem permite que sejam
modeladas tanto a parte de processos quanto a de dados das arquiteturas
de controle.
2. Utilização combinada de ferramentas de checagem de modelos: FDR para
as especificações da parte CSP e SPARK para as especificações da parte
Object-Z, sendo estas últimas verificadas no nível de código.
3. Implementação em RavenSPARK dos canais de comunicação CSP. A im-
plementação utilizada neste trabalho foi adaptada dos trabalhos de Atiya
(2004) e Atiya e King (2005), uma vez que nestes trabalhos a implementa-
ção dos canais leva em conta apenas o padrão Ravenscar, sendo utilizadas
construções proíbidas na linguagem SPARK como tipos de dados genéri-
cos. Estes tiveram de ser removidos, sendo necessárias algumas adaptações
no código gerado a fim de permitir o uso da linguagem SPARK, além de
facilitar a verificação do código desenvolvido.
4. Utilização de padrões da linguagem Ada específicos para uso em sistemas
críticos, que são a linguagem SPARK e o perfil Ravenscar. Isso faz com
que o código gerado seja mais robusto e determinístico, uma vez que estes
padrões restringem a utilização de diversos recursos da linguagem Ada que
podem levar a erros de difícil detecção, principalmente os relacionados aos
aspectos de concorrência no sistema.
1.4 Organização do Trabalho
24
1.4
Organização do Trabalho
No capítulo a seguir serão apresentados alguns conceitos básicos utilizados
neste trabalho, como por exemplo uma breve descrição sobre métodos formais e
a linguagem CSP-OZ.
O capítulo 3 apresenta uma descrição detalhada do método de desenvolvi-
mento proposto, finalizando com um exemplo completo de sua aplicação por
meio de um modelo simplificado de Produtor / Consumidor.
Em seguida, no capítulo 4 pode ser vista uma descrição completa do sistema
de controle de ROVs em desenvolvimento, que inclui o veículo submarino e sua
estação de controle.
Por fim, temos os resultados e as conclusões deste trabalho nos capítulos 6 e
7, respectivamente.
No Anexo A pode ser visto o script em CSPM utilizado na verificação do
modelo da arquitetura de controle na ferramenta FDR, enquanto que no Anexo
B podem ser vistos todos os códigos fontes em RavenSPARK da implementação da
arquitetura, que foram verificados utilizando o examinador da linguagem SPARK
e posteriormente compilados e embarcados num computador PC104 executando
o sistema operacional VxWorks.
Um resumo das notações das linguagens CSP e Object-Z pode ser visto no
Apêndice A.
25
2
Conceitos Básicos
Neste capítulo serão apresentados alguns conceitos utilizados neste trabalho.
O início da discussão estará relacionado à modelagem de software, onde serão bre-
vemente descritas as linguagens de modelagem utilizadas incluindo CSP, Object-Z
e sua combinação: CSP-OZ. Também será apresentada superficialmente a UML-
RT, que atualmente é a linguagem mais utilizada na modelagem de software pela
indústria. Por fim, será apresentado um breve resumo sobre arquiteturas de con-
trole, de modo a elucidar algumas das escolhas de projeto adotadas na arquitetura
desenvolvida no capítulo 5.
2.1
Modelagem de Software
No desenvolvimento de projetos de software, certamente a modelagem re-
presenta a parte mais importante. Isso porque ela auxilia no desenvolvimento da
estrutura do sistema, o que possibilita a criação de projetos mais robustos, expan-
síveis e de fácil manutenção. Entretanto, em muitos projetos não são utilizados
nenhuma técnica de modelagem ou de análise do sistema em desenvolvimento,
cabendo ao programador ir construindo os componentes do sistema à medida
que as necessidades vão aparecendo. Tal abordagem é conhecida na literatura
como "bottom-up" . Neste trabalho será utilizada uma abordagem inversa, onde
primeiramente são especificados todos os componentes do sistema, e também os
seus modos de interação, para só depois ser feita sua implementação por meio de
uma linguagem de programação. Portanto, será dada grande ênfase na fase de
modelagem do software.
2.2
UML-RT
Atualmente, a UML ( Unified Modelling Language) é a linguagem para es-
pecificação de modelos mais utilizada na indústria. UML-RT (UML for Real
Time Systems) é uma extensão da UML projetada para descrever arquiteturas
2.2 UML-RT
26
de sistemas embarcados (AKHLAKI et al., 2006). Apesar do nome Real Time suge-
rir tempo, o foco desta extensão consiste na modelagem da estrutura de sistemas
distribuídos, e não na inserção de facilidades para a inserção do conceito de tempo
nas especificações.
UML-RT define três construções para a modelagem da estrutura de sistemas
distribuídos, que são (FISCHER; OLDEROG; WEHRHEIM, 2001):
Cápsulas Descrevem componentes complexos do sistema que podem interagir
com o ambiente. Elas podem ser estruturadas hierarquicamente, agrupando
diversas subcápsulas que por sua vez também podem conter outras subcáp-
sulas.
Portas A interação das cápsulas com o ambiente é feita por meio de portas.
Estas geralmente estão associadas a protocolos, que determina o fluxo de
informação através das portas.
Conectores Estes são usados para conectar duas ou mais portas de cápsulas, e
assim descrever as relações de comunicação entre as cápsulas do sistema.
Com estes elementos, as diversas partes do sistema podem ser projetadas de
forma independente, contanto que cada parte respeite as interfaces de comunica-
ção existentes nos protocolos.
A utilização de UML-RT no desenvolvimento de sistemas embarcados apre-
senta algumas vantagens. A mais notável delas é a utilização de uma notação
gráfica e amplamente difundida para a especificação de modelos de software. En-
tretanto, sua principal desvantagem é a falta de uma semântica precisa, o que
abre espaço para ambiguidades na interpretação dos modelos por parte dos pro-
gramadores, e também dificulta a elaboração de provas sobre o comportamento
do sistema. Para sanar essa dificuldade foi desenvolvida a OCL (OMG, 2003), que
permite a inserção de invariantes e pré e pós condições de métodos nas classes.
Além da utilização da OCL, pode ser feita uma combinação da UML com
outras linguagens formais para a eliminação de ambiguidades. Segundo Borges
e Mota (2007), existem diversos trabalhos na área de métodos formais relacio-
nados à sua integração com UML. Um exemplo destes trabalhos é o de Polido
(2007), que propõe regras de refinamento entre especificações feitas em UML-RT
para especificações em CSP-OZ. Do ponto de vista da Engenharia de Software, a
integração de métodos formais no processo de desenvolvimento propicia aos dia-
gramas UML uma semântica precisa, o que possibilita sua verificação, e também
2.3 Métodos Formais
27
estabelece uma relação entre o modelo gráfico de mais alto nível e a implemen-
tação final. Isso porque as especificações formais permitem que sejam geradas
condições de verificação das especificações do modelo antes de sua implementa-
ção. Do ponto de vista dos métodos formais, a vantagem de uma combinação
com UML é a possibilidade de se especificar graficamente algumas da caracterís-
ticas comportamentais, estruturais e de orientação a objetos de um sistema em
conjunto com as notações matemáticas. A especificação formal pode então ser
obtida parcialmente com base nos diagramas UML por meio de regras de mape-
amento, de modo a complementar a especificação do modelo desenvolvido. Isso
poderia aumentar a aceitação do uso de uma linguagem de especificação formal
(MOLLER et al., 2008) em áreas onde seu uso ainda é incomum, como por exemplo
no desenvolvimento de software embarcado para robôs submarinos.
Neste trabalho não será utilizado esse tipo de abordagem. A modelagem do
sistema será feita utilizando-se métodos formais, mais precisamente utilizando a
linguagem CSP-OZ, cabendo à UML apenas os diagramas de casos de uso na
elaboração dos requisitos do sistema.
2.3
Métodos Formais
Técnicas que utilizam princípios matemáticos para desenvolver sistemas com-
putacionais são denominados de modo geral como Métodos Formais. A idéia de
se especificar o que um sistema computacional deve fazer utilizando notação e
técnicas de manipulação matemática é o que se denomina especificação formal
(LIGHTFOOT, 1991). Uma especificação formal é uma descrição de um software
ou hardware, que pode ser utilizada tanto para uma implementação quanto para
a realização de testes. A especificação é diretamente focada no aspecto compor-
tamental do programa, ou seja, no “o que” o programa faz, e não no aspecto
operacional, que seria o “como” o programa é implementado. As expressões ma-
temáticas têm a vantagem de serem precisas e não ambíguas, o que elimina con-
fusões e a necessidade de discussões sobre o significado de uma especificação.
Outra grande vantagem consiste na concisão das expressões matemáticas, o que
se torna relevante na especificação de sistemas de maior tamanho e complexidade
(LIGHTFOOT, 1991).
A idéia do uso de especificações formais é que seja garantida a corretude do
sistema por construção, ou seja, que sejam encontrados e corrigidos erros mais
comuns já na fase de projeto, sendo que esta corretude é garantida através de
formalismo matemático. Isso minimizaria o problema de se depurar erros no
2.3 Métodos Formais
28
software que está em uso no sistema embarcado, uma vez que segundo Hall e
Chapman (2002), a maior parte deles já seria identificada e resolvida no início do
projeto. Esta identificação precoce de erros também implica em menores custos
de projeto, uma vez que torna-se bem mais complicado corrigí-los à medida que o
projeto vai avançando (BOWEN; HINCHEY, 2005; HALL; CHAPMAN, 2002; AMEY,
2002). Existem diversas linguagens de especificação formal, como Z, Object Z,
VDM, B, entre outras. Neste trabalho será utilizada a linguagem CSP-OZ, que
é uma união da álgebra de processos CSP com a linguagem Object Z, e que
será apresentada na seção 2.3.3. Um aspecto considerável na utilização desta
linguagem é o fato de Z e CSP serem dois dos formalismos mais utilizados na
indústria (BORGES; MOTA, 2007).
A principal vantagem do uso de métodos formais na especificação de software
consiste na capacidade de se analisar a especificação, com o objetivo de se assegu-
rar da presença e/ou ausência de propriedades em seu comportamento (SHERIF;
SAMPAIO; CAVALCANTE, 2001). Uma abordagem para se alcançar este objetivo
é utilizar ferramentas para checagem de modelos1, que permitem comparar au-
tomaticamente os comportamentos observados em um sistema com relação à sua
especificação. No caso deste trabalho, a interação entre os processos que consti-
tuem o sistema será verificada formalmente com a utilização da ferramenta FDR
(SYSTEMS, 2005), da Formal Systems.
Conforme mostrado nos trabalho de Brooks (1987) e Hall e Chapman (2002),
devido às dificuldades inerentes ao processo de desenvolvimento de software,
torna-se impossível garantir a ausência de erros em qualquer projeto por meio
de testes. No caso de sistemas embarcados, este problema apresenta um agra-
vante devido à dificuldade de realizar a detecção e depuração de erros no caso
de uma falha. É neste sentido que vem sendo proposto o desenvolvimento de
software tendo como ferramenta o uso de métodos formais, visando auxiliar na
verificação e validação de modelos para a eliminação de erros na especificação do
software, pois aproximadamente 80% dos erros de software são gerados nessa fase
de projeto (BOWEN; HINCHEY, 2005).
Apesar de todas as vantagens apresentadas, o seu emprego apresenta um custo
elevado. Uma das razões é que para sua utilização é necessário haver mão de obra
altamente especializada, o que aumenta os custos de projeto. O desenvolvimento
das especificações também aumenta consideravelmente a fase de modelagem do
sistema, o que acaba atrasando as demais fases do projeto. Porém, com um uso
correto, o emprego de métodos formais pode reduzir consideravelmente o período
1em inglês, essa técnica é conhecida como Model Checking.
2.3 Métodos Formais
29
de testes.
Já existe um consenso na comunidade de software de que a especificação
é essencial. Porém, em qual grau? A resposta depende de quão crítico é o
sistema (ATIYA, 2004). Na área de Sistemas Críticos, existem normas que visam
a regulamentação do modo com que os softwares são desenvolvidos. Um exemplo
destas é a DO-178B (RTCA, 1992), utilizada no desenvolvimento de softwares
aviônicos. Segundo ela, para se atingir os níveis mais críticos de confiabilidade, é
recomendado o uso de métodos formais no desenvolvimento do software. Já pela
norma inglesa DEF STAN 00-55, o uso de métodos formais é mandatório tanto
no projeto do sistema quanto como complemento aos testes e análises estáticas
(BOWEN; HINCHEY, 2005).
2.3.1
CSP
CSP ( Communicating Sequential Process) (ROSCOE; HOARE; BIRD, 1997) é
uma álgebra de processos que pode ser utilizada como método formal de especifi-
cação de concorrência e dinâmica de sistemas. Ela apresenta um conjunto básico
de operadores que permitem modelar diversos aspectos presentes em sistemas
concorrentes como paralelismo, não determinismo, sincronização de processos,
entre outras coisas. Segundo Schneider (1999), esta abordagem tem sido empre-
gada na especificação, análise e verificação de sistemas concorrentes de tempo
real, atuando como ferramenta para lidar com os problemas que podem surgir
com a presença de concorrência.
O conceito básico adotado em CSP é considerar os processos como entidades
independentes, com interfaces particulares sobre as quais eles podem interagir
com o ambiente. Com isso é possível também formar composições, pois se dois
processos são combinados para formar um sistema maior, novamente este sistema
é considerado independente e com uma interface maior, ou seja, um processo
maior. A interface de um processo é representada pelo conjunto de eventos que
podem ser recebidos ou enviados. Tomemos como exemplo um processo P, cuja
interface seria composta pelos eventos {a, b, c}. Sua especificação em CSP po-
deria ser P = a → b → c → P, onde o processo ficaria em loop infinito. Sua
máquina de estados pode ser vista na figura 2.1.
A principal vantagem do uso de CSP é a possibilidade de verificação do modelo
desenvolvido por meio da ferramenta de checagem de modelos FDR (SYSTEMS,
2005). Segundo Lawrence (2005), a verificação de projetos com o FDR em certos
casos específicos onde o sistema é pequeno pode resultar em um nível considerável
2.3 Métodos Formais
30
Figura 2.1: Máquina de estados da especificação CSP do processo P.
de confiança na corretude dos mesmos, mas não se pode provar essa corretude
se o sistema aumenta muito em tamanho devido à limitações na capacidade de
análise da ferramenta. Como neste trabalho não serão feitas análises na estrutura
de dados do sistema com o FDR, este problema de explosão no número de estados
não ocorrerá. Como serão feitas apenas checagens com relação à parte dinâmica
do sistema, ou seja, na comunicação entre os processos, o número de estados é
relativamente pequeno e perfeitamente tratável pela ferramenta.
2.3.2
Object-Z
Object Z é baseado na linguagem de especificação formal Z (LIGHTFOOT,
1991), e provê construções específicas para facilitar especificações em um estilo
orientado a objetos (DUKE; ROSE, 2000). Nesta linguagem, cada classe pode ser
examinada e entendida isoladamente, e classes complexas podem ser especificadas
em termos de outras mais simples através do mecanismo de herança da progra-
mação orientada a objetos. O objetivo de sua utilização é a possibilidade de se
especificar as estruturas de dados do sistema por meio de uma linguagem de alto
nível, sem se preocupar inicialmente com detalhes de implementação.
A estrutura básica de uma classe em Object-Z é:
Nome
definição de tipos e constantes
esquema de estados
esquema de inicialização de estados
esquema de operações
Para ilustrar o uso da linguagem, será mostrada a especificação de uma pi-
lha capaz de armazenar elementos do tipo genérico T , com capacidade máxima
indicada pela constante size (especificação 2.3.2). Logo, esta pilha possui uma
capacidade máxima de dez elementos. Representando os elementos da pilha, te-
2.3 Métodos Formais
31
Stack [ T ]
size : N
[class constants]
size = 10
elements : seq T
[class attributes]
# elements ≤ size
[class invariants]
INIT
elements =
[inicial conditions]
push
∆( elements)
[Delta list]
item? : T
[method parameters]
# elements < size
elements = item?
elements
pop
∆( elements)
item! : T
elements =
item! = head elements
elements = tail elements
Especificação 2.1: Especificação de uma Pilha em Object-Z.
2.3 Métodos Formais
32
mos o atributo elements, que consiste em uma sequência (ou seja, um conjunto
ordenado) de elementos do tipo T , que no estado inicial da classe não possui
nenhum elemento, ou seja, a pilha inicia-se vazia.
Para manipulação da mesma, podem ser utilizados os métodos push e pop, que
retiram e adicionam elementos no início da pilha, respectivamente. No método
push, para que seja possível adicionar o elemento item?, o número de elementos
existentes na pilha deve ser menor do que o seu tamanho. Caso essa condição
seja satisfeita, item? é adicionado no início da pilha. Assim como em CSP, os
decoradores “?” e “!” indicam variável recebida do ambiente e variável retornada
ao ambiente, respectivamente. Já o método pop retorna primeiro elemento da
pilha ( item!) caso esta não esteja vazia, removendo em seguida este elemento da
pilha.
O exemplo acima serviu apenas para ilustrar superficialmente como seria uma
especificação em Object-Z. Maiores detalhes sobre como construir especificações
completas nessa linguagem podem ser encontradas em Duke e Rose (2000).
2.3.3
CSP-OZ
CSP-OZ (FISCHER, 1997; FISCHER; WEHRHEIM, 2000; FISCHER, 2000) é uma
linguagem de especificação de alto nível criada para a descrição de sistemas dis-
tribuídos.
Conforme descrito acima, Object-Z é uma extensão da linguagem Z orientada
a objetos destinada à especificação dos objetos de um sistema. Uma classe em
Object-Z consiste na especificação de um espaço de estados e das operações neste
espaço. A álgebra de processos CSP foi desenvolvida para descrever o comporta-
mento dinâmico de um sistema. A idéia básica de CSP-OZ é definir a semântica
de uma classe utilizando o modelo semântico de CSP. Portanto, todos os opera-
dores de CSP podem ser utilizados para combinar objetos, e a sintaxe de CSP e
Object-Z podem ser misturadas. A semântica de um processo em CSP é baseada
em seu alfabeto, ou seja, no conjunto de eventos que este pode observar do am-
biente. Já em Object-Z, os eventos observáveis de uma classe são seus métodos
com seus respectivos parâmetros.
O objetivo principal de CSP-OZ é dar às classes em Object-Z a semântica de
CSP. Como consequência, as classes são um modo alternativo de descrição de um
processo de CSP, ou seja, classes em CSP-OZ são a versão orientada a objetos
de um processo CSP (FISCHER, 2000). Essa visão mais voltada à orientação a
2.4 Arquiteturas de Controle
33
objetos facilita a implementação de uma maneira simples e transparente. Sendo
assim, adiciona-se à estrutura básica de uma especificação em Object-Z a definição
dos canais de comunicação da classe e a especificação de seu comportamento em
CSP, que consiste na especificação da ordem em que estes métodos e canais são
utilizados.
Descrições mais completas da linguagem podem ser encontradas em Fischer
(1997) e Fischer (2000).
2.4
Arquiteturas de Controle
Por volta do final da década de 80, a tendência na área de robôs inteligentes
era projetar e programar segundo o paradigma reativo. O paradigma reativo per-
mitiu que robôs utilizando processadores de baixo custo e com pouca memória
fossem capazes de operar em tempo real. Entretanto, o custo da reatividade era
que o sistema eliminava qualquer tipo de planejamento ou funções que envol-
vessem um conhecimento do estado global do robô em relação ao seu ambiente.
Ou seja, o robô não seria capaz de planejar trajetórias otimizadas (planejamento
de trajetória), construir mapas, monitorar seu próprio desempenho ou mesmo
selecionar os comportamentos necessários no cumprimento de uma dada tarefa.
Segundo Murphy (2000), o novo desafio da inteligência artificial no início dos anos
90 era como colocar planejamento e deliberação de volta nos robôs, porém sem
perder o sucesso obtido com o controle reativo. O consenso era que o controle
comportamental era o modo "correto"de se fazer o controle de baixo nível, de-
vido ao seu sucesso e elegância como teoria computacional tanto para inteligência
biológica e de máquinas.
Arquiteturas que utilizam comportamentos reativos, mas que também incor-
poram planejamento, são conhecidas como parte do paradigma “Híbrido Delibe-
rativo/Reativo”. Segundo Murphy (2000), as híbridas são a melhor solução geral
de arquitetura por duas razões: primeiro, o uso de técnicas de processamento
assíncrono ( multi-tasking, threads, etc.) permitem que as tarefas deliberativas
executem independentemente dos comportamentos reativos. Isso implica, por
exemplo, que um planejador pode calcular a próxima trajetória do robô de uma
forma mais lenta, enquanto que o robô continua reagindo a estímulos rapida-
mente, com os comportamentos trabalhando a uma frequência maior; segundo,
uma boa modularidade de software permite que subsistemas ou objetos em uma
arquitetura híbrida sejam misturados e/ou ativados para aplicações específicas.
Com isso, aplicações em que se exige comportamento puramente reativo poderiam
2.4 Arquiteturas de Controle
34
Figura 2.2: Esquema de funcionamento do paradigma Híbrido.
ser abordadas utilizando-se apenas uma parte da arquitetura híbrida, enquanto
que em uma aplicação onde se exigiria um maior grau de inteligência do robô se
utilizaria a arquitetura completa.
Conceitualmente, ela é dividida em duas partes: uma reativa e a outra delibe-
rativa. A organização de um sistema híbrido pode ser descrita como: PLANEJA,
e então SENTE-AGE, como pode ser visto na figura 2.2. O PLANEJA inclui toda
a deliberação e modelagem do mundo, e não apenas planejamento de caminhos
ou tarefas. Essa separação deve-se ao planejamento consumir muito tempo de
processamento, e portanto ele deve ser desacoplado da execução de tempo real.
Primeiramente, o robô planeja como executar a missão (utilizando um modelo
do ambiente) ou uma tarefa. Em seguida, ele inicializa ou ativa um conjunto
de comportamentos ( SENTE-AGE ) para executar o plano. Os comportamentos
executarão até que o plano esteja completo, para que então o planejador gere um
novo conjunto de comportamentos, e assim por diante.
A grande vantagem no desenvolvimento de uma arquitetura híbrida é a pos-
sibilidade da junção das vantagens presentes tanto em arquiteturas deliberativas
quanto em reativas. Segundo Simpson, Jacobsen e Jadud (2006), uma aborda-
gem puramente hierárquica para controle de robôs está focada principalmente no
aspecto de planejamento de um ciclo comportamental do robô. Neste ciclo, pri-
meiramente ele recebe informações do ambiente. Em seguida planeja sua próxima
ação baseado nessas informações, para somente então executar alguma ação uti-
lizando seu conjunto de atuadores. Em cada ciclo, o robô planeja explicitamente
sua próxima ação a partir do conhecimento reunido do ambiente. A desvanta-
gem deste tipo de abordagem é que ela não propicia uma separação de tarefas,
e pode introduzir dependências entre camadas de funcionalidade, além de inserir
um atraso relativamente alto entre o sensoriamento e a atuação se comparado ao
paradigma comportamental.
Dentro do paradigma reativo, um dos principais modos é a arquitetura Sub-
2.4 Arquiteturas de Controle
35
sumption (BROOKS, 1986). Nessa arquitetura, a percepção do ambiente e o pla-
nejamento para a execução de um determinado comportamento interagem di-
retamente uns com os outros. A construção de sistemas de controle de robôs
é feita por meio de níveis crescentes de competência, onde cada nível adicional
é construído com base em um nível pré-existente, ou pelo menos interage com
níveis pré-existentes, para que a cada novo nível sejam inseridas novas compe-
tências e que a junção de todos os níveis (ou camadas) determinem o sistema
como um todo. Com o uso correto de supressores e inibidores (que são definidos
em seu trabalho), o sistema pode variar entre vários modos de operação diferen-
tes dependendo das entradas do ambiente, fazendo uma melhor re-utilização de
módulos já escritos e bem testados. A idéia é remover estruturas de controle
centralizadas. A partir de comportamentos simples e da interação entre eles e o
ambiente, podem surgir comportamentos resultantes mais complexos. Isso traz a
vantagem de tornar o projeto de sistemas robóticos mais simples e o código en-
volvido mais robusto, uma vez que o sistema é composto de vários componentes
pequenos e simples. Entretanto, a principal critica à este paradigma de controle
consiste na dificuldade de se definir os comportamentos necessários, e também de
se desenvolver o sistema de um modo linear de modo a aproveitar a vantagem de
desenvolvimento incremental.
No contexto deste trabalho, a utilização da arquitetura Subsumption apre-
senta grandes vantagens relacionadas à verificação e implementação dos modelos
desenvolvidos para a arquiteturas de controle de veículos submarinos. A pri-
meira delas já foi mencionada, que é a divisão do sistema em diversos processos
menores, que por sua vez apresentam máquinas de estados menores, facilitando
assim o processo de análise com o FDR. Outra vantagem consiste na facilidade
de correlação entre os processos da arquitetura Subsumption com os processos de
CSP. Isso porque assim como em CSP, na arquitetura Subsumption o sistema é
composto por diversos processos que executam de maneira concorrente entre si,
se comunicando exclusivamente por meio de canais.
Neste trabalho será desenvolvida uma arquitetura híbrida, porém sendo im-
plementada apenas sua parte reativa. A camada deliberativa, cujo processo prin-
cipal é o Autonomous, será implementada em trabalhos futuros. A camada reativa
será projetada seguindo-se as idéias da arquitetura Subsumption, de modo que o
veículo evite colisões ao se movimentar. Entretanto, essa característica não será
efetivamente testada, pois não existem sensores embarcados no robô utilizado
capazes de detectar obstáculos no ambiente.
2.5 Conclusões do Capítulo
36
2.5
Conclusões do Capítulo
Neste capítulo foram apresentados alguns dos conceitos básicos utilizados no
trabalho relacionados a linguagens de modelagem de software (em especial às
linguagens formais) e a arquiteturas de controle.
Foi visto que a UML é atualmente o padrão utilizado na indústria. Porém, a
utilização desta linguagem pode levar a ambiguidades no modelo desenvolvido em
função da falta de uma semântica precisa em alguns de seus diagramas. A fim de
se amenizar este problema, foi criada a OCL, além de existirem diversos trabalhos
que propõem uma união da UML com linguagens formais. Neste trabalho, para
a modelagem da arquitetura de controle desenvolvida utilizou-se a linguagem
formal CSP-OZ, possibilitando assim a especificação de seus processos e de toda
a estrutura de dados utilizada, além de possibilitar que o modelo seja analisado
com auxílio da ferramenta FDR a fim de se indentificar deadlocks, livelocks e
checar seu determinismo.
Com relação à arquitetura de controle, esta foi desenvolvida segundo o pa-
radigma híbrido. Assim, ela foi dividida em duas camadas conceituais: uma
deliberativa, onde é estipulado o próximo movimento do robô; e uma reativa,
onde estão presentes as funções básicas de sobreviência e funcionamento do robô.
A vantagem dessa abordagem consiste na separação das atividades, e assim as
funções de sobrevivência podem ser executadas a uma frequência maior, enquanto
que as demais funções menos críticas podem levar mais tempo para serem pro-
cessadas.
37
3
Método de Desenvolvimento
Neste trabalho está sendo proposto um método para o desenvolvimento ro-
busto de software embarcado para veículos submarinos. Esse baseia-se no uso de
métodos formais para a especificação do sistema, juntamente com ferramentas de
checagem do modelo desenvolvido e de sua implementação. Conforme mostrado
na figura 3.1, ele é composto de três fases, que podem ser divididas em etapas
sequenciais.
M O D E L A G E M D O S I S T E M A
D i a g r a m a d e
Especificação dos
Verificação
Estrutura
Componentes
do Modelo
I M P L E M E N T A Ç Ã O D O M O D E L O
Geração de
Anotações
Verificação da
Código
SPARK
I m p l e m e n t a ç ã o