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.

Este trabalho de pesquisa propõe um Método Dirigido por Modelos para a Documentação e Análise (MDM-DA) de requisitos de Sistemas Computadorizados - SC, visando melhorar a qualidade e a eficácia na documentação da execução de atividades da Engenharia de Requisitos, e manter rastreabilidade entre os elementos produzidos durante o ciclo de desenvolvimento destes sistemas. Além disso, um Modelo Conceitual para aplicação do MDM-DA foi projetado, considerando-se os conceitos teóricos de Engenharia de Sistemas e Engenharia de Requisitos. Concebeu-se o MDM-DA com um total de 12 passos estruturados, considerando-se: as características do Desenvolvimento Dirigido por Modelos (Model-Driven Development - MDD) para se representar os requisitos graficamente; a Linguagem de Modelagem de Sistemas (System Modeling Language - SysML) para modelagem, especificação e documentação de requisitos; e o Método de Análise Kano para priorização/negociação dos requisitos. Adicionalmente, para propiciar um conjunto de análises detalhadas de todo o processo de desenvolvimento, o MDM-DA propõe 5 (cinco) métricas e 6 tabelas de requisitos da SysML. Durante esta pesquisa, concebeu-se também um Protótipo da Extensão do profile da SysML, denominado PExSys, visando contemplar as novas construções visuais necessárias para operacionalização do MDM-DA. O método foi aplicado com sucesso em 3 (três) componentes de um projeto real, denominado Projeto FINEP 5206/06 - Projeto de Integração e Cooperação Amazônica para a Modernização do Monitoramento Hidrológico (ICA-MMH). Finalmente, dentre as principais vantagens que se percebe com a aplicação do MDM-DA, podem-se citar: uma otimização na documentação e na rastreabilidade entre os modelos produzidos; um aumento da eficácia na comunicação tanto entre os membros envolvidos na equipe de desenvolvimento quanto na comunicação desta equipe com os stakeholders do SC; e a realização de análises detalhadas de todo o processo de desenvolvimento.

Esta pesquisa aborda o desenvolvimento do AndroMDT, um Método de Testes Funcionais Dirigido por Modelos para Sistemas de Software. Este método se apoia nas características do Desenvolvimento Dirigido por Testes (Test Driven Development - TDD) e da Arquitetura Dirigida por Modelos (Model Driven Architecture - MDA). Nele, descreve-se a aplicação do método AndroMDT em um componente de software, envolvendo um estudo de caso de um projeto real. Esta pesquisa propiciou a especificação, execução, documentação e análise de testes funcionais. Além disso, foi possível obter-se rastreabilidade entre os elementos mais relevantes do estudo de caso, desde os requisitos até os artefatos de teste produzidos.

Muitos projetos de software falham devido à má estruturação e execução do processo de Engenharia de Requisitos (ER) e na maioria dos casos o fator humano inserido nesta atividade é crucial para a falha, pois são atividades essencialmente humanas e subjetivas. Com o intuito de auxiliar o ser humano na execução e contribuir para a melhora do processo da ER, prevenindo ou minimizando alguns de seus problemas, tais como, perda de requisitos e incompleteza, esse trabalho propõe analisar esses problemas sob a ótica de teorias do erro humano. Para isso realiza-se um levantamento dos erros e problemas principais, verifica-se a ocorrência dos erros no processo da ER, através da aplicação de questionários aos especialistas da área, efetua-se um mapeamento entre os erros e problemas, estima-se a chance de ocorrência do erro dada a presença do problema e sugerem-se soluções para esses erros com o intuito de solucionar os problemas do processo avaliado. A abordagem proposta deu origem a um método de diagnóstico que lista em ordem de prioridade os erros que podem estar ocorrendo no processo avaliado. Objetivando validar a abordagem, são feitos testes com especialistas da área da ER através do uso de um protótipo em formato de página web. Os questionários mostraram que os erros humanos ocorrem nas atividades do processo da ER e que existem erros que possuem um grau elevado de importância para o processo. A validação com os especialistas mostrou que a abordagem é válida, pois auxilia na organização e na percepção de lacunas do processo.

Objetivo do trabalho é propor um processo para a Análise de Stakeholders utilizando mapas cognitivos a fim de auxiliar no processo da elicitação de necessidades raiz. O processo proposto aborda desde o estudo do contexto até a identificação das necessidades e informações relevantes para serem transformadas em requisitos e a estruturação do problema a partir do ponto de vista do stakeholder. A motivação do trabalho vem da dificuldade no entendimento das necessidades dos stakeholders no desenvolvimento de sistemas, sejam eles produto, processo ou serviço. O processo proposto se fundamenta nos conceitos da Engenharia de Sistemas e da Cognição e seus Mapas Cognitivos. O trabalho aporta três principais contribuições, a primeira é a elicitação exaustiva com o stakeholder até chegar à necessidade raiz, utilizando o processo cognitivo por meio dos repetidos questionamento até chegar à raiz do assunto. A segunda contribuição é na captura gráfica do rationale das necessidades mais relevantes. A terceira contribuição é a de ajudar ao stakeholder a entender sua própria necessidade e/ou problema, também com a ajuda do processo cognitivo utilizado na criação dos mapas. De esta maneira obtendo como resultado informações relevantes elicitadas junto com seu rationale e o entendimento do problema. O processo proposto foi aplicado num estudo piloto dentro do Laboratório de Integração e Testes (LIT) do Instituto Nacional de Pesquisas Espaciais (INPE). O Processo de Análise de Stakeholders Utilizando Mapas Cognitivos pode ser considerado como uma opção válida na hora de decidir a estratégia da Análise de Stakeholders; ele facilita a aproximação com o stakeholder e fornece uma ferramenta iterativa e interativa que abre a porta para a imaginação tanto para o stakeholder expressar suas necessidades quanto para que o engenheiro de sistemas possa gerar questionamentos e ambos construírem conclusões do problema e seu contexto dando partida à concepção da solução.

Nas últimas décadas constatou-se o uso cada vez mais massivo de sistemas computadorizados principalmente em setores da indústria aeronáutica. Na busca pelo aumento de eficiência no desenvolvimento, recomenda-se o uso do Desenvolvimento Baseado em Modelos (MBD). Este trabalho de pesquisa propõe um Método para Modelagem de Sistemas, denominado M2S, como forma de se bene?ciar da modelagem do sistema desde os estágios iniciais de concepção do sistema. Esta abordagem visa diminuir o ciclo de vida de desenvolvimento e aumentar a qualidade das especi?cações. Nesse sentido, o método proposto se baseia na Linguagem de Modelagem de Sistemas (SysML), no Processo Uni?cado (RUP), no uso de Ambientes Integrados de Engenharia de Software Auxiliada por Computador (I-CASE-E) e na geração automática de código. Após combinar estes elementos num conjunto de passos que compõe o método proposto, realizou-se por meio de um estudo de caso a veri?cação da aplicação do método. O estudo de caso envolveu o desenvolvimento de um protótipo do Sistema de Dados Anemométricos (Air Data System - ADS), com dois experimentos. Foi possível constatar a facilidade em segregar as fases de desenvolvimento, realizar a evolução gradual das especi?cações e modelos, para ?nalmente se chegar a transformação dos modelos independentes de plataforma em código fonte e se constituir o protótipo. Aplicou-se testes e métricas de Halstead, de Linhas de Código e de Complexidade Ciclomática como forma de comparar os dois experimentos.

Estuda-se o problema de sintonia de controladores, objetivando-se a formulação do problema de sintonia ótima de controladores. Busca-se uma formulação que seja geral, ou seja, válida para qualquer estrutura de controlador e qualquer conjunto de especificações. São abordados dois temas principais: especificação de controladores e sintonia ótima de controladores. São compiladas as principais formas de especificação e avaliação de controladores e é feita a formulação do problema de sintonia de controladores como um problema padrão de otimização. A abordagem proposta e os conceitos apresentados são então aplicados em um conjunto de exemplos. / The problem of control tuning is studied, aiming the formulation of the optimal control tuning problem. A general formulation, valid for any controller structure and any set of specifications, is sought. Two main themes are addressed: controller specification and optimal controller tuning. The main ways of controller specification and assessment are compiled and the optimal controller tuning problem is formulated as a standard optimization problem. The proposed approach and the presented concepts are then applied in a set of examples.

O ajuste de modelos de regressão beta requer a especificação de uma função de ligação. Algumas funções de ligação úteis são: logito, probito, complemento log-log e log-log. Usualmente, a ligação logito é utilizada pois permite interpretação simples para os parâmetros de regressão. O principal objetivo deste trabalho é avaliar o impacto da especificação incorreta da função de ligação em regressão beta. Estudos de simulação serão usados com esse prop´osito. Amostras da variável resposta serão geradas assumindo uma função de ligação conhecida (verdadeira) e o modelo de regressão beta será ajustado usando a função de ligação verdadeira (correta) e algumas funções de ligação incorretas. Resultados numéricos serão comparados para avaliar o efeito da especificação incorreta da função de ligação sobre as inferências em regressão beta. Adicionalmente, será introduzido um modelo de regressão beta com função de ligação de Aranda-Ordaz, a qual depende de um parâmetro que pode ser estimado através dos dados. / Fitting beta regression models requires the specification of the link function. Some useful link functions for beta regression are: logit, probit, complementary log-log and log-log. Usually, the logit link is used since it allows easy interpretation for the regression parameters. The main objective of this work is to evaluate the impact of misspecification of the link function in beta regression. Simulation studies will be used for this purpose. Samples of the response variable will be generated assuming a known (true) link function, and the beta regression will be fitted using the true (correct) link and some incorrect link functions. Numerical results will be compared to evaluate the effect of misspecification of the link function on inference in beta regression. Also, we will introduce a beta regression model with Aranda-Ordaz link function, which depends on an unknown parameter that can be estimated through the data.

Esta dissertação apresenta o levantamento e definição dos requisitos necessários para um sistema de monitoramento de veículos no transporte rodoviário de cargas, cujo custo de implantação seja acessível a grande parte das empresas. Para isso são aplicados alguns métodos da Engenharia de Requisitos, tais como: Vord, Preview e Volere. O conjunto de requisitos obtido através deste levantamento é então utilizado como fonte para a especificação de requisitos do sistema proposto. / This dissertation shows the survey and definition of the necessary requirements regarding a monitoring system for vehicles that transport goods via roads, whose low cost implementation is accessible for most of the companies. For this purpose, some methods of the Engineering of Requirements are applied, such as: Vord, Preview and Volere. The set of requirements gotten via this survey is the source for the specification of requirements of the proposed system.

Com a presença cada vez maior de sistemas computacionais e novas tecnologias no cotidiano das pessoas, garantir que eles não falhem e funcionem corretamente tornou-se algo de extrema importância. Além de indicar a qualidade do sistema, assegurar seu bom funcionamento é essencial para se evitar perdas, desde financeiras até de vidas. Uma das técnicas utilizadas para esta finalidade é a chamada verificação formal de programas. A partir da especificação do sistema, descrita numa linguagem formal, são definidas propriedades a serem satisfeitas e que certificariam a qualidade do software. Estas propriedades devem então ser implementadas para uso num verificador, que é a ferramenta responsável por executar a verificação e informar quais propriedades foram satisfeitas e quais não foram; no caso das propriedades terem sido violadas, o verificador deve indicar aos desenvolvedores os possíveis locais com código incorreto no sistema. A desvantagem do uso da verificação formal é, além do seu alto custo, a necessidade de haver pessoas com experiência em métodos formais para definir propriedades a partir da especificação formal do sistema, e convertê-las numa representação que possa ser entendida pelo verificador. Este processo de definição de propriedades é particularmente complexo, demorado e suscetível a erros, por ser feito em sua maior parte de forma manual. Para auxiliar os desenvolvedores na utilização da verificação formal em programas escritos em Java, propomos neste trabalho a geração de representação de propriedades para uso direto num verificador. As propriedades a serem geradas são objetivos de teste derivados da especificação formal do sistema. Estes objetivos de teste descrevem o comportamento esperado do sistema que deve ser observado durante sua execução. Ao estabelecer que o universo de propriedades corresponde ao universo de objetivos de teste do programa, garantimos que as propriedades geradas em nosso trabalho descrevem o comportamento esperado do programa por meio de caminhos de execução que levam a um estado de aceitação da propriedade, ou a um estado de violação. Assim, quando o verificador checa o objetivo de teste, ele consegue dar como resultado o veredicto de sucesso ou falha para a propriedade verificada, além de dados da cobertura dos caminhos de execução do programa que podem ser usados para análise do comportamento do programa que levou ao sucesso ou falha da propriedade verificada. / The task of guaranteeing that computational systems do not fail and work correctly has become extremely important with the growing presence of new technologies in people\'s lives. Therefore, it is essential to ensure that such systems work properly to confirm their high-quality and to avoid financial and even life losses. One of the techniques used to this purpose is called formal verification of programs. From the system specification, which should be described in a formal language, we define properties that must be satisfied during system execution to guarantee the software quality. Then, these properties are checked using a verifier, which is the tool responsible for running the verification and for notifying whether the property was satisfied by the program; if the property was violated, it indicates to software developers the possible location of faults in the system. The disadvantages of using formal verification are the high cost to apply this technique in practice, and the necessity of having people with experience in formal methods to derive the properties from system specification and define them in a formal representation that can be read by a program verifier. This particular task of deriving a property from system specification and defining it to be checked by a verifier is complex, time-consuming and error-prone, since it is usually done by hand. To help software developers in the application of formal verification in Java programs, we propose in this work the generation of properties formal representation for direct use in a verifier. The generated properties are test purposes, which are derived from system formal specification and present the desirable system behavior that must be observed during the system execution. Establishing that the universe of properties correspond to the universe of test purposes of a program, we guarantee that the generated properties describe the expected program behavior through execution traces that lead to either an accept state or a refuse state. Thus, when the verifier checks the test purpose, it can give a success/fail verdict for the property, and provide traces coverage data that can be used to analyze the program behavior that led to that verdict.