Checagem de arquiteturas de controle de veículos submarinos: uma abordagem baseada em... por Fábio Henrique de Assis - Versão HTML

ATENÇÃO: Esta é apenas uma visualização em HTML e alguns elementos como links e números de página podem estar incorretos.
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.

index-16_1.jpg

index-16_2.jpg

index-16_3.jpg

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.

index-19_1.jpg

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

index-30_1.jpg

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

index-34_1.png

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