O emprego de técnicas de controle para veículos submarinos, envolve muitas questões de interesse prático e teórico. Neste trabalho apresenta-se o desenvolvimento de um sistema de controle inteligente e adaptativo a ser aplicado na navegação de veículos submarinos semi-autônomos (VSSAs). Utiliza-se uma técnica baseada no controle nebuloso (fuzzy), visando gerenciar o veículo submarino no controle de velocidade, profundidade, orientação e na evasão de obstáculos. A operação de veículos submarinos usando a técnica proposta, exige a definição, análise e tratamento de um vasto conjunto de comandos complexos manipulados pelo controlador. A metodologia utilizada divide a ação de controle em 3 fases. A primeira trata do posicionamento inicial do veículo submarino, a segunda fase trata da sua navegação e a fase final de gerenciar o comportamento do veículo próximo da posição-objetivo. A implementação funcional do controlador e dividida em módulos. O primeiro módulo informa o comportamento do ambiente e do próprio veículo, fornecendo dados iniciais sobre seu posicionamento e sua profundidade; um segundo módulo trata da presença de obstáculos em diferentes direções com dados fornecidos por sonares e assim determina as ações para a evasão de obstáculos. A ação de controle e estabelecida usando conceitos da teoria nebulosa (fuzzy) no universo de discurso, através de variáveis lingüísticas e de regras de inferência definidas a partir do conhecimento de especialistas, que envolvem a imprecisão característica do comportamento humano. As informações no final do processo são concentradas, de forma que a ação de controle e determinada para que possa enviar sinais de controle aos atuadores. / The design of underwater vehicle involves a very large number of practical and theoretical problems. In this work, it is tackled the development of a intelligent and adaptive controller, to be used in the navigation of semi-autonomous underwater vehicles (SAUV). To achieve this goal, a technique based on the fuzzy theory was employed to control the vehicle movements, including the evasion of obstacles. The operation of underwater vehicles using this approach demands the definition and treatment of a vast set of complex commands, manipulated by the controller. The control action is subdivided into three stages, the first one deals the control action during the initial positioning of the vehicle, a second stage deals with the navigation itself and the final stage deals the control action when the vehicle is close to the objective-position. The functional development of the controller was also subdivided into modules. The first module deals with the management of input data such as environmental disturbances and initial vehicle position, such as depth of the vehicle. The second module deals the detection of obstacles in different directions and the optimal evasion action to avoid collisions. The control action during a mission is established using concepts of the Fuzzy theory in the universe of speech, through linguistic variables and rules of inference defined from the knowledge of specialists, involving the characteristic imprecision of human behavior. In the end of the process, the information is defuzzificated, so that control actions are determined, allowing a practical implementation.

Este trabalho trata do controle dos movimentos de um Veículo Submersível Autônomo (VSA). Veículos submersíveis são difíceis de controlar devido à alta não linearidade de seus modelos, ao forte acoplamento de movimentos, ao desconhecimento de certas dinâmicas, às incertezas do próprio modelo, devido a distúrbios externos impostos pelo ambiente e devido ao ruído de sensores. A dificuldade de controle pode ser exacerbada quando o veículo é subatuado. Para realização deste trabalho foi escolhido um VSA do tipo torpedo, cujo modelo matemático disponível na literatura foi devidamente modificado para garantir uma melhor descrição de seus movimentos em seis graus de liberdade (6-GL). O modelo foi então validado através de simulações numéricas. Para a síntese dos controladores utilizou-se uma técnica de controle avançada. Mais especificamente, utilizou-se a abordagem do controle H1 para sistemas multivariáveis. Assim foram obtidos controladores centralizados capazes de superar o problema do forte acoplamento de movimentos. Técnicas de controle avançado permitem também considerar as informações disponíveis sobre perturbações, incertezas, ruídos e diferentes tipos de entrada já na fase de síntese, o que permite obter controladores com desempenho adequado numa ampla faixa de operação. Neste trabalho, em particular, a técnica da Sensibilidade Mista foi escolhida para a síntese de controladores robustos. Nesta abordagem, formatam-se algumas funções de malha fechada ligadas a sensibilidade do sistema buscando garantir estabilidade e desempenho robusto para o sistema controlado. Usando a mesma técnica de controle desenvolveu-se ainda um controlador de dois graus de liberdade (2-GL), apropriado para aplicação no problema de guiagem, onde procura-se seguir trajetórias tridimensionais. Os controladores desenvolvidos foram testados em simulações numéricas, produzindo-se uma grande quantidade de resultados. A análise destes resultados revela o poder e flexibilidade das técnicas escolhidas. / This work focuses the motion control of an Autonomous Underwater Vehicle (AUV). Underwater vehicles are difficult to control due to high non-linearities of its model, coupling between dynamics, unknown dynamics, model uncertainties, disturbances and sensor noises. Difficulty is greater, when the system is subactuated. In this work, a mathematical model of a torpedo-like AUV available in the bibliography was chosen and refined, leading to a six degree of freedom (6-DOF) model. The model was further analyzed and validated by a number of numerical simulations. Advanced approaches were used for the synthesis of controllers. Speciffically, a H1 approach for multivariable systems was used. Thus, a centralized controller was developed, able to avoid the problem of high coupling between the variables. This advanced approach is also able to use informations about perturbations, uncertainties, noises and different types of input signals in the synthesis stage, leading to controllers with better performance in a large operation bandwidth. In this work, a Mixed Sensitivity approach was employed. This control approach is based on the shapping of well known closed-loop sensitivity functions, seeking to achieve stability and performance robustness. Using a similar technique, a controller with two degree of freedom (2-DOF) was also synthesised, to tackle the guidance problem tracking of 3-D trajectories was then fully achieved. The controllers developed were tested in a number of numerical simulations. Analyses of results reveals the power and flexibility of the employed techniques.

Os veículos submarinos não tripulados tem uma importância crescente devido à sua flexibilidade e baixo custo. Devido à sua complexidade intrínseca, eles requerem diversas competências diferentes para serem desenvolvidos e permitem realizar pesquisas em vários campos do conhecimento. No contexto de uma universidade, que possui pessoal heterogêneo e de alta rotatividade, faz-se mister adotar uma organização que permita que os esforços de cada aluno possam ser reusados pelos outros, de modo as atividades de pesquisa possam avançar com pouca perda de tempo e retrabalho. Tal necessidade pode ser respondida pela aplicação de conceitos da engenharia de sistemas, tais como modularidade, separação formal entre soluções tecnológicas e necessidades, classificação funcional, critérios para escolha do método de desenvolvimento, uso de referencial normativo técnico, plano tecnológico, integração, verificação e validação e gerenciamento de configurações. Este trabalho se limita a desenvolver uma arquitetura de controle, observando os conceitos de engenharia de sistemas, aplicada a um AUV. É feita uma comparação com outras arquiteturas similares do estado da arte e mostram-se resultados de testes em piscina para esta arquitetura. É mostrado também que foi possível estabelecer a continuidade do desenvolvimento por outros alunos, validando a utilidade da metodologia. Conclui-se que, para aumentar a eficiência da pesquisa universitária, é necessário observar aspectos gerenciais e institucionais além dos aspectos técnicos ao conceber soluções técnicas. / The unmanned underwater vehicles have a growing position due to their flexibility and low cost. Due to their inherent complexity, they require many different skills to be developed and they allow conducting research in various fields of knowledge. In the context of a university, which has heterogeneous staff and high turnover, there is the need of adopting an organization that allows the efforts of each student be reused by others, so research activities can proceed with little loss of time and rework. This need can be answered by the application of system engineering concepts such as modularity, formal separation between technology solutions and needs, functional classification, criteria for the choice of development method, use of technical reference standard, technological plan, integration, verification and validation and configuration management. This work is limited to development of a control architecture, observing the concepts of systems engineering, applied to an AUV. A comparison is made with other similar architectures in the state of the art and shows up test results in the pool for this architecture. It is also shown that it was possible to keep the development by other students, validating the utility of the methodology. It is concluded that in order to increase the efficiency of university research, it must be observed managerial and institutional aspects beyond the technical aspects when designing technical solutions.

Este trabalho trata da aplicação de técnicas de identificação de sistemas dinâmicos a ensaios com veículos submarinos não tripulados ou com modelos em escala auto-propelidos de veículos submarinos. Complementa-se, desta forma as investigações que vêm sendo realizadas no Laboratório de Veículos Não Tripulados, LVNT, voltadas à estimativa de parâmetros hidrodinâmicos de veículos autônomos submarinos, AUVs. Estas têm utilizado os métodos pertencentes a outras classes de abordagens para a estimativa de modelos de manobras para veículos submarinos como os métodos CFD e ASE (de BARROS, et. al., 2004, 2006, 2008a, 2008b; de BARROS e DANTAS, 2012). Outras atribuições deste trabalho dizem respeito à compreensão e desenvolvimento na modelagem linear da dinâmica de manobra de veículos submarinos, teoria e implementação de métodos de identificação de sistemas aplicados a resultados de ensaios com modelos auto-propelidos. As atividades de estudo foram divididas de acordo com os temas relativos à dinâmica de veículos submarinos, conceitos físicos envolvidos nas derivadas hidrodinâmicas de estabilidade, técnicas de identificação de sistemas e aspectos tecnológicos e experimentais da utilização de ensaios com modelos auto-propelidos. As atividades voltadas ao atendimento de tais metas envolveram, durante o programa de pesquisa, estudos de modelos analíticos, simulação numérica do movimento, realização de experimentos em piscina e campo com um AUV, e a implementação de ferramentas numéricas de análise de dados e estimação de parâmetros de manobra. / This paper is related to the application of techniques for identifying dynamic systems testing scale models of underwater vehicles or even unmanned underwater vehicles in real scale. Complementing in this way the investigations that have been conducted in the Laboratory of Unmanned Vehicles, LVNT, aimed to estimate the hydrodynamic parameters of autonomous underwater vehicles, AUVs. They have used the methods belonging to the three other classes mentioned (of Barros, et. Al., 2004, 2006, 2008a, 2008b; Barros and the DANTAS, 2012). Other tasks of this work relates to the understanding and development in modeling linear dynamic manoeuvring underwater vehicles, theory and implementation of identification methods applied to systems test results with self-propelled models. The study activities were divided according to themes related to the dynamics of underwater vehicles, physical concepts derived in the hydrodynamic stability, system identification techniques and technological aspects and experimental trials with use of self-propelled models. The activities aimed at meeting those goals involved during the research program, studies of analytical models, numerical simulation of the movement, performing experiments with a swimming pool and AUV, and implementation of numerical tools for data analysis and parameter estimation maneuver.

O uso de modelos de manobras representa um auxilio importante no projeto de veículos marinhos, permitindo a verificação do desempenho destes veículos, desenvolver o sistema de piloto automático, dentre outras aplicações durante a fase de projeto. Na área de veículos submarinos, seus modelos são tradicionalmente baseados em equações de movimento que incluem expressões polinomiais para representar os esforços hidrodinâmicos. Estes modelos são derivados de uma expansão em série de Taylor de forças e momentos, sendo representados em função das variáveis de movimento. Entretanto, estes modelos limitam a representatividade dos esforços hidrodinâmicos, e, especialmente para os termos de segunda ou mais altas ordens, eles requerem ensaios custosos em tanque de provas para identificar corretamente cada um dos coeficientes polinomiais. Esta dependência em ensaios de tanque de provas tem um impacto critico, ou até mesmo não realístico, durante o desenvolvimento de veículos autônomos submarinos, AUVs, de baixo ou médio custo. Utilizando métodos atuais da fluidodinâmica computacional (CFD), este trabalho propõe um roteiro alternativo para definir os modelos de manobras não lineares para uma classe de AUVs. As simulações de CFD, verificados e validados por normas rigorosas, são utilizados como base para derivar as funções não lineares que representam os esforços hidrodinâmicos, devido variações na velocidade lateral, velocidade angular e deflexão dos lemes. A abordagem numérica é complementada pelo uso de modelos analíticos e semi-empíricos oriundos da indústria de mísseis, que tiveram que ser melhorados com informações retiradas das simulações de CFD. Ajustes adicionais e derivações nos intervalos de confiança para as estimativas produzidas por métodos numéricos também são fornecidos pelo uso de modelos analíticos e semi-empíricos. Adotando o AUV Pirajuba como caso de estudo, a validação dos modelos de manobra foi realizada em duas etapas. Primeiro, são comparadas as estimativas dos esforços hidrodinâmicos com as medições em tanque de provas de um modelo cativo, e em seguida a resposta dinâmica dos modelos de manobras são comparadas com aquelas obtidas por ensaios em mar, sempre utilizando critérios de verificação e validação. Este tipo de análise indicou uma validação dos esforços hidrodinâmicos e do movimento para grande parte dos ensaios, sendo que nos demais casos o AUV teve seu comportamento dinâmico bem reproduzido. Este resultado demonstra que a metodologia proposta pode ser utilizada para estimar o modelo de manobra de um AUV típico, gerando uma solução de menor custo para a fase de desenvolvimento destes veículos. / The use of maneuvering models represents an important assistance in the project of marine vessels, allowing for the evaluation of the vehicle performance, the autopilot system development, among other tasks during the design phase. In the field of underwater vehicles, those models commonly are based on equations of motion that include polynomial expressions for representing the hydrodynamic efforts. They are derived from Taylor series expansion of forces and moments represented as functions of the motion variables. However, those models limit the representativeness of the hydrodynamic efforts, and, especially for the second order or higher terms, they require expensive trials in towing tank facilities to correctly identify each polynomic coefficient. This dependence on intensive tank tests has a critical impact, or is even unrealistic during the development of middle or low cost autonomous underwater vehicles, AUVs. Using current methods of computational fluid dynamics (CFD), this work proposes an alternative roadmap to construct nonlinear manoeuvring models, which can be applied to a class of AUVs. CFD simulations, verified and validated by rigorous standards, are used as basis to derive nonlinear functions that represent the hydrodynamic efforts due to variations in lateral velocity, angular rate and rudder deflection. The numerical approach is complemented by the use of analytical and semi-empirical models derived from missile industry, which have been improved according to the information taken from the CFD simulations. Further adjustments and derivation of confidence intervals to the estimates produced by the numerical method are also provided by the use of analytical and semi-empirical models. Adopting the Pirajuba AUV as a test bed, the manoeuvring model validation was carried out in two stages. Firstly, estimates of hydrodynamic efforts are compared with measurements obtained from experiments using a captive model in a towing tank. In the second step, the dynamic response predicted by the maneuvering model was compared with the output measured during free model trials. This type of analysis validated the hydrodynamic efforts and motion in most of the experiments, whereas for the remaining cases the AUV had its dynamic behavior well reproduced. This result demonstrates that the proposed methodology can be used to estimate the maneuvering model of a typical type AUV, generating a lower cost solution for the development phase of the vehicle.

Este trabalho trata do controle dos movimentos de um Veículo Submersível Autônomo (VSA). Veículos submersíveis são difíceis de controlar devido à alta não linearidade de seus modelos, ao forte acoplamento de movimentos, ao desconhecimento de certas dinâmicas, às incertezas do próprio modelo, devido a distúrbios externos impostos pelo ambiente e devido ao ruído de sensores. A dificuldade de controle pode ser exacerbada quando o veículo é subatuado. Para realização deste trabalho foi escolhido um VSA do tipo torpedo, cujo modelo matemático disponível na literatura foi devidamente modificado para garantir uma melhor descrição de seus movimentos em seis graus de liberdade (6-GL). O modelo foi então validado através de simulações numéricas. Para a síntese dos controladores utilizou-se uma técnica de controle avançada. Mais especificamente, utilizou-se a abordagem do controle H1 para sistemas multivariáveis. Assim foram obtidos controladores centralizados capazes de superar o problema do forte acoplamento de movimentos. Técnicas de controle avançado permitem também considerar as informações disponíveis sobre perturbações, incertezas, ruídos e diferentes tipos de entrada já na fase de síntese, o que permite obter controladores com desempenho adequado numa ampla faixa de operação. Neste trabalho, em particular, a técnica da Sensibilidade Mista foi escolhida para a síntese de controladores robustos. Nesta abordagem, formatam-se algumas funções de malha fechada ligadas a sensibilidade do sistema buscando garantir estabilidade e desempenho robusto para o sistema controlado. Usando a mesma técnica de controle desenvolveu-se ainda um controlador de dois graus de liberdade (2-GL), apropriado para aplicação no problema de guiagem, onde procura-se seguir trajetórias tridimensionais. Os controladores desenvolvidos foram testados em simulações numéricas, produzindo-se uma grande quantidade de resultados. A análise destes resultados revela o poder e flexibilidade das técnicas escolhidas. / This work focuses the motion control of an Autonomous Underwater Vehicle (AUV). Underwater vehicles are difficult to control due to high non-linearities of its model, coupling between dynamics, unknown dynamics, model uncertainties, disturbances and sensor noises. Difficulty is greater, when the system is subactuated. In this work, a mathematical model of a torpedo-like AUV available in the bibliography was chosen and refined, leading to a six degree of freedom (6-DOF) model. The model was further analyzed and validated by a number of numerical simulations. Advanced approaches were used for the synthesis of controllers. Speciffically, a H1 approach for multivariable systems was used. Thus, a centralized controller was developed, able to avoid the problem of high coupling between the variables. This advanced approach is also able to use informations about perturbations, uncertainties, noises and different types of input signals in the synthesis stage, leading to controllers with better performance in a large operation bandwidth. In this work, a Mixed Sensitivity approach was employed. This control approach is based on the shapping of well known closed-loop sensitivity functions, seeking to achieve stability and performance robustness. Using a similar technique, a controller with two degree of freedom (2-DOF) was also synthesised, to tackle the guidance problem tracking of 3-D trajectories was then fully achieved. The controllers developed were tested in a number of numerical simulations. Analyses of results reveals the power and flexibility of the employed techniques.

Os veículos submarinos não tripulados tem uma importância crescente devido à sua flexibilidade e baixo custo. Devido à sua complexidade intrínseca, eles requerem diversas competências diferentes para serem desenvolvidos e permitem realizar pesquisas em vários campos do conhecimento. No contexto de uma universidade, que possui pessoal heterogêneo e de alta rotatividade, faz-se mister adotar uma organização que permita que os esforços de cada aluno possam ser reusados pelos outros, de modo as atividades de pesquisa possam avançar com pouca perda de tempo e retrabalho. Tal necessidade pode ser respondida pela aplicação de conceitos da engenharia de sistemas, tais como modularidade, separação formal entre soluções tecnológicas e necessidades, classificação funcional, critérios para escolha do método de desenvolvimento, uso de referencial normativo técnico, plano tecnológico, integração, verificação e validação e gerenciamento de configurações. Este trabalho se limita a desenvolver uma arquitetura de controle, observando os conceitos de engenharia de sistemas, aplicada a um AUV. É feita uma comparação com outras arquiteturas similares do estado da arte e mostram-se resultados de testes em piscina para esta arquitetura. É mostrado também que foi possível estabelecer a continuidade do desenvolvimento por outros alunos, validando a utilidade da metodologia. Conclui-se que, para aumentar a eficiência da pesquisa universitária, é necessário observar aspectos gerenciais e institucionais além dos aspectos técnicos ao conceber soluções técnicas. / The unmanned underwater vehicles have a growing position due to their flexibility and low cost. Due to their inherent complexity, they require many different skills to be developed and they allow conducting research in various fields of knowledge. In the context of a university, which has heterogeneous staff and high turnover, there is the need of adopting an organization that allows the efforts of each student be reused by others, so research activities can proceed with little loss of time and rework. This need can be answered by the application of system engineering concepts such as modularity, formal separation between technology solutions and needs, functional classification, criteria for the choice of development method, use of technical reference standard, technological plan, integration, verification and validation and configuration management. This work is limited to development of a control architecture, observing the concepts of systems engineering, applied to an AUV. A comparison is made with other similar architectures in the state of the art and shows up test results in the pool for this architecture. It is also shown that it was possible to keep the development by other students, validating the utility of the methodology. It is concluded that in order to increase the efficiency of university research, it must be observed managerial and institutional aspects beyond the technical aspects when designing technical solutions.

O emprego de técnicas de controle para veículos submarinos, envolve muitas questões de interesse prático e teórico. Neste trabalho apresenta-se o desenvolvimento de um sistema de controle inteligente e adaptativo a ser aplicado na navegação de veículos submarinos semi-autônomos (VSSAs). Utiliza-se uma técnica baseada no controle nebuloso (fuzzy), visando gerenciar o veículo submarino no controle de velocidade, profundidade, orientação e na evasão de obstáculos. A operação de veículos submarinos usando a técnica proposta, exige a definição, análise e tratamento de um vasto conjunto de comandos complexos manipulados pelo controlador. A metodologia utilizada divide a ação de controle em 3 fases. A primeira trata do posicionamento inicial do veículo submarino, a segunda fase trata da sua navegação e a fase final de gerenciar o comportamento do veículo próximo da posição-objetivo. A implementação funcional do controlador e dividida em módulos. O primeiro módulo informa o comportamento do ambiente e do próprio veículo, fornecendo dados iniciais sobre seu posicionamento e sua profundidade; um segundo módulo trata da presença de obstáculos em diferentes direções com dados fornecidos por sonares e assim determina as ações para a evasão de obstáculos. A ação de controle e estabelecida usando conceitos da teoria nebulosa (fuzzy) no universo de discurso, através de variáveis lingüísticas e de regras de inferência definidas a partir do conhecimento de especialistas, que envolvem a imprecisão característica do comportamento humano. As informações no final do processo são concentradas, de forma que a ação de controle e determinada para que possa enviar sinais de controle aos atuadores. / The design of underwater vehicle involves a very large number of practical and theoretical problems. In this work, it is tackled the development of a intelligent and adaptive controller, to be used in the navigation of semi-autonomous underwater vehicles (SAUV). To achieve this goal, a technique based on the fuzzy theory was employed to control the vehicle movements, including the evasion of obstacles. The operation of underwater vehicles using this approach demands the definition and treatment of a vast set of complex commands, manipulated by the controller. The control action is subdivided into three stages, the first one deals the control action during the initial positioning of the vehicle, a second stage deals with the navigation itself and the final stage deals the control action when the vehicle is close to the objective-position. The functional development of the controller was also subdivided into modules. The first module deals with the management of input data such as environmental disturbances and initial vehicle position, such as depth of the vehicle. The second module deals the detection of obstacles in different directions and the optimal evasion action to avoid collisions. The control action during a mission is established using concepts of the Fuzzy theory in the universe of speech, through linguistic variables and rules of inference defined from the knowledge of specialists, involving the characteristic imprecision of human behavior. In the end of the process, the information is defuzzificated, so that control actions are determined, allowing a practical implementation.

O desenvolvimento de arquiteturas de controle para veículos submarinos é uma tarefa complexa. Estas podem ser caracterizadas pelos seguintes atributos: tempo real, multitarefa, concorrência e comunicações distribuídas em rede. Neste cenário, existem múltiplos processos sendo executados em paralelo, possivelmente distribuídos, e se comunicando uns com os outros. Neste contexto, o modelo comportamental pode levar a fenômenos como deadlocks, livelocks, disputa 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 modelos de arquiteturas de controle de veículos submarinos baseado em Especificações Formais. A linguagem de especificação formal escolhida foi CSP-OZ, uma combinaçã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 propriedades 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, livelocks, 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 juntamente 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 Remotamente) é 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. / The development of control architectures for Underwater Vehicles is a complex task. These control architectures might be chracterised by the following attributes: real-time, multitasking, concurrency, and distributed over communication 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, livelocks, 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 Sequential Process) is a process algebra developed to describe behavioural models of parallel process. The model checking of formal specifications is a task of reasoning 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 language 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 (originally 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 specifications must first be converted into a SPARK language code, together with proper annotations, and then model checking can be realised in code. The development 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.

O uso de modelos de manobras representa um auxilio importante no projeto de veículos marinhos, permitindo a verificação do desempenho destes veículos, desenvolver o sistema de piloto automático, dentre outras aplicações durante a fase de projeto. Na área de veículos submarinos, seus modelos são tradicionalmente baseados em equações de movimento que incluem expressões polinomiais para representar os esforços hidrodinâmicos. Estes modelos são derivados de uma expansão em série de Taylor de forças e momentos, sendo representados em função das variáveis de movimento. Entretanto, estes modelos limitam a representatividade dos esforços hidrodinâmicos, e, especialmente para os termos de segunda ou mais altas ordens, eles requerem ensaios custosos em tanque de provas para identificar corretamente cada um dos coeficientes polinomiais. Esta dependência em ensaios de tanque de provas tem um impacto critico, ou até mesmo não realístico, durante o desenvolvimento de veículos autônomos submarinos, AUVs, de baixo ou médio custo. Utilizando métodos atuais da fluidodinâmica computacional (CFD), este trabalho propõe um roteiro alternativo para definir os modelos de manobras não lineares para uma classe de AUVs. As simulações de CFD, verificados e validados por normas rigorosas, são utilizados como base para derivar as funções não lineares que representam os esforços hidrodinâmicos, devido variações na velocidade lateral, velocidade angular e deflexão dos lemes. A abordagem numérica é complementada pelo uso de modelos analíticos e semi-empíricos oriundos da indústria de mísseis, que tiveram que ser melhorados com informações retiradas das simulações de CFD. Ajustes adicionais e derivações nos intervalos de confiança para as estimativas produzidas por métodos numéricos também são fornecidos pelo uso de modelos analíticos e semi-empíricos. Adotando o AUV Pirajuba como caso de estudo, a validação dos modelos de manobra foi realizada em duas etapas. Primeiro, são comparadas as estimativas dos esforços hidrodinâmicos com as medições em tanque de provas de um modelo cativo, e em seguida a resposta dinâmica dos modelos de manobras são comparadas com aquelas obtidas por ensaios em mar, sempre utilizando critérios de verificação e validação. Este tipo de análise indicou uma validação dos esforços hidrodinâmicos e do movimento para grande parte dos ensaios, sendo que nos demais casos o AUV teve seu comportamento dinâmico bem reproduzido. Este resultado demonstra que a metodologia proposta pode ser utilizada para estimar o modelo de manobra de um AUV típico, gerando uma solução de menor custo para a fase de desenvolvimento destes veículos. / The use of maneuvering models represents an important assistance in the project of marine vessels, allowing for the evaluation of the vehicle performance, the autopilot system development, among other tasks during the design phase. In the field of underwater vehicles, those models commonly are based on equations of motion that include polynomial expressions for representing the hydrodynamic efforts. They are derived from Taylor series expansion of forces and moments represented as functions of the motion variables. However, those models limit the representativeness of the hydrodynamic efforts, and, especially for the second order or higher terms, they require expensive trials in towing tank facilities to correctly identify each polynomic coefficient. This dependence on intensive tank tests has a critical impact, or is even unrealistic during the development of middle or low cost autonomous underwater vehicles, AUVs. Using current methods of computational fluid dynamics (CFD), this work proposes an alternative roadmap to construct nonlinear manoeuvring models, which can be applied to a class of AUVs. CFD simulations, verified and validated by rigorous standards, are used as basis to derive nonlinear functions that represent the hydrodynamic efforts due to variations in lateral velocity, angular rate and rudder deflection. The numerical approach is complemented by the use of analytical and semi-empirical models derived from missile industry, which have been improved according to the information taken from the CFD simulations. Further adjustments and derivation of confidence intervals to the estimates produced by the numerical method are also provided by the use of analytical and semi-empirical models. Adopting the Pirajuba AUV as a test bed, the manoeuvring model validation was carried out in two stages. Firstly, estimates of hydrodynamic efforts are compared with measurements obtained from experiments using a captive model in a towing tank. In the second step, the dynamic response predicted by the maneuvering model was compared with the output measured during free model trials. This type of analysis validated the hydrodynamic efforts and motion in most of the experiments, whereas for the remaining cases the AUV had its dynamic behavior well reproduced. This result demonstrates that the proposed methodology can be used to estimate the maneuvering model of a typical type AUV, generating a lower cost solution for the development phase of the vehicle.