Detectar e analisar malwares é um processo essencial para aprimorar os sistemas de segurança. As soluções atuais apresentam limitações no processo de investigação e detecção de códigos maliciosos sofisticados. Mais do que utilizar técnicas para evadir sistemas de análise, malwares sofisticados requerem condições específicas no ambiente em que são executados para revelar seu comportamento malicioso. Com o surgimento das Redes Definidas por Software (SDN), notou-se uma oportunidade para aprimorar o processo de investigação de malware propondo uma arquitetura flexível apta a detectar variações comportamentais de maneira automática. Esta tese apresenta uma arquitetura especializada para analisar códigos maliciosos que permite controlar de maneira unificada o ambiente de análise, incluindo o sandbox e os elementos que o circundam. Dessa maneira, é possível gerenciar regras de contenção, configuração dinâmica de recursos, e manipular o tráfego de rede gerado pelos malwares. Para avaliar a arquitetura foi analisado um conjunto de malwares em dois cenários de avaliação. No primeiro cenário de avaliação, as funcionalidades descritas pela solução proposta revelaram novos eventos comportamentais em 100% dos malwares analisados. Já, no segundo cenários de avaliação, foi analisado um conjunto de malwares projetados para dispositivos IoT. Em consequência, foi possível bloquear ataques, monitorar a comunicação do malware com seu controlador de botnet, e manipular comandos de ataques. / Mechanisms to detect and analyze malicious software are essential to improve security systems. Current security mechanisms have limited success in detecting sophisticated malicious software. More than to evade analysis system, many malware require specific conditions to activate their actions in the target system. The flexibility of Software-Defined Networking (SDN) provides an opportunity to develop a malware analysis architecture that can detect behavioral deviations in an automated way. This thesis presents a specialized architecture to analyze malware by managing the analysis environment in a centralized way, including to control the sandbox and the elements that surrounds it. The proposed architecture enables to determine the network access policy, to handle the analysis environment resource configuration, and to manipulate the network connections performed by the malware. To evaluate our solution we have analyzed a set of malware in two evaluation scenarios. In the first evaluation scenario, we showed that the mechanisms proposed have increased the number of behavioral events in 100% of the malware analyzed. In the second evaluation scenario, we have analyzed malware designed for IoT devices. As a result, by using the MARS features, it was possible to block attacks, to manipulate attack commands, and to enable the malware communication with the respective botnet controller. The experimental results showed that our solution can improve the dynamic malware analysis process by providing this configuration flexibility to the analysis environment.

[pt] A apresentação de aplicações hipermídia dinâmicas pode ser vista em alguns casos como um processo de autoria recursivo, no qual aplicações são recriadas em tempo de apresentação quando modificações no conteúdo são desencadeadas por interações entre a máquina de apresentação e outras entidades (tais como usuários, objetos imperativos, aplicações externas etc.). Em alguns cenários de aplicações hipermídia dinâmicas, é possível identificar um padrão de composição hipermídia que se mantém mesmo após o documento ter sido recriado. Aplicações desse tipo são comuns, por exemplo, em um ambiente de TV Digital Interativa. A existência de um padrão durante a apresentação de uma aplicação para TV Digital Interativa permite estabelecer uma analogia entre os processos de recriar documentos dinamicamente e de especificar aplicações pelo método orientado a templates. Nesse último método, o autor especifica uma aplicação preenchendo lacunas deixadas por um template que representa o padrão de composição hipermídia da aplicação. Analogamente, na recriação dinâmica de documentos o módulo que processa atualizações no documento faz o papel de preencher as lacunas de templates. O objetivo principal do presente trabalho é definir uma arquitetura, inspirada nessa analogia, para estruturar aplicações NCL que podem ser refatoradas dinamicamente e que se mantêm em conformidade com seus respectivos templates. Nested Context Language (NCL) é a linguagem para autoria de aplicações do Sistema Brasileiro de TV Digital terrestre. Para validar a solução proposta, foram desenvolvidas uma aplicação que captura um cenário real de uso e uma ferramenta de autoria que permite especificar graficamente o preenchimento de templates. / [en] The presentation of dynamic hypermedia applications may be seen as a recursive authoring process, in which applications are recreated during presentation time, whenever content changes are triggered by interactions between the presentation engine and other entities such as users, imperative objects, external applications, etc. In some scenarios of dynamic hypermedia applications, it is possible to identify a hypermedia composition pattern that remains consistent even after the document is recreated. This kind of applications is common, for instance, in an Interactive Digital Television environment. The presence of such a pattern throughout the presentation of an application for Interactive Digital Television allows the establishment of an analogy between recreating documents dynamically and authoring applications through a template-driven authoring method. Using the latter, the authoring process is conducted by filling gaps left by a template that represents the hypermedia composition pattern of an application. Analogously, in the dynamic document re-creation, the module that processes document updates fulfills the role of filling the templates gaps. The main goal of the present work is to define an architecture, inspired by this analogy, to structure NCL applications that can be dynamically refactored and that remain conform to their respective templates. Nested Context Language (NCL) is the language of Brazilian System of Digital Terrestrial Television applications. In order to validate the proposal, an application that captures a real scenario and an authoring tool for specify graphically document filling was developed.

Desde o início do século XXI, vivenciamos uma explosão na produção de informações de diversos tipos, tais como fotos, áudios, vídeos, entre outros. Dentre essas informações, existem aquelas em que a informação pode ser dividida em partes menores, mas que devem ser relacionadas seguindo uma ordem total. Um exemplo deste tipo de informação é um arquivo de vídeo que foi dividido em dez segmentos identificados com números de 1 a 10. Para reproduzir o vídeo original a partir dos segmentos é necessário que seus identificadores estejam ordenados. A estrutura denominada tabela de hash distribuída (DHT) tem sido amplamente utilizada para armazenar, atualizar e recuperar esse tipo de informação de forma eficiente em diversos cenários, como monitoramento de sensores e vídeo sob demanda. Entretanto, a DHT apresenta problemas de escalabilidade quando um membro da estrutura não consegue atender as requisições recebidas, trazendo como consequência a inacessibilidade da informação. Este trabalho apresenta uma arquitetura em camadas denominada MATe, que trata o problema da escalabilidade em dois níveis: estendendo a DHT com a introdução de agentes baseados na utilidade e organizando a quantidade de requisições solicitadas. A primeira camada trata a escalabilidade ao permitir a criação de novos agentes com o objetivo de distribuir as requisições evitando que um deles tenha a escalabilidade comprometida. A segunda camada é composta por grupos de dispositivos organizados de tal forma que somente alguns deles serão escolhidos para fazer requisições. A arquitetura foi implementada para dois cenários onde os problemas de escalabilidade acontecem: (i) monitoramento de sensores; e (ii) vídeo sob demanda. Para ambos cenários, os resultados experimentais mostraram que MATe melhora a escalabilidade quando comparada com as implementações originais da DHT. / Since the beginning of the 21st century, we have experienced an explosive growth in the generation of information, such as photos, audios, videos, among others. Within this information, there are some in which the information can be divided and related following a total order. For example, a video file can be divided into ten segments identified with numbers from 1 to 10. To play the original video from these segments, their identifiers must be fully ordered. A structure called Distributed Hash Table (DHT) has been widely used to efficiently store, update, and retrieve this kind of information in several application domains, such as video on demand and sensor monitoring. However, DHT encounters scalability issues when one of its members fails to answer the requests, resulting in information loss. This work presents MATe, a layered architecture that addresses the problem of scalability on two levels: extending the DHT with the introduction of utility-based agents and organizing the volume of requests. The first layer manages the scalability by allowing the creation of new agents to distribute the requests when one of them has compromised its scalability. The second layer is composed of groups of devices, organized in such a way that only a few of them will be chosen to perform requests. The architecture was implemented in two application scenarios where scalability problems arise: (i) sensor monitoring; and (ii) video on demand. For both scenarios, the experimental results show that MATe improves scalability when compared to original DHT implementations.

Submitted by Santos Davilene (davilenes@ufba.br) on 2016-05-25T14:04:00Z No. of bitstreams: 1 FINAL Dissertação Mestrado - Hugo Sica de Andrade.pdf: 4068482 bytes, checksum: f4538e19111b94a4c1caae39a4e6c525 (MD5) / Made available in DSpace on 2016-05-25T14:04:00Z (GMT). No. of bitstreams: 1 FINAL Dissertação Mestrado - Hugo Sica de Andrade.pdf: 4068482 bytes, checksum: f4538e19111b94a4c1caae39a4e6c525 (MD5) / O paradigma de Linhas de Produto de Software (LPS) tem provado ser um meio efetivo para se obter reuso de grande escala em diferentes domínios. A abordagem tira proveito de aspectos comuns entre diferentes produtos, enquanto também considera propriedades específicas dos mesmos. A arquitetura tem um papel importante na engenharia de LPS, provendo meios para melhor entender e manter o ambiente de derivação de produtos. No entanto, é difícil evoluir tal arquitetura, pois nem sempre é claro onde e como refatorar. A arquitetura de uma LPS contém um modelo que irá resultar na arquitetura de produtos, e muitas vezes inclui soluções que indicam um design (arquitetural) inadequado. Uma forma de avaliar tais decisões de design é através da identificação de bad smells de arquitetura, ou seja, propriedades que prejudicam a qualidade do software, mas não são necessariamente errôneas ou representam falhas. Nesse sentido, o objetivo desta dissertação é obter um melhor entendimento de bad smells de arquitetura em LPSs. Primeiramente, o estado-da-arte atual em Arquiteturas de Linhas de Produto de software (ALP) é investigado através de um estudo de mapeamento sistemático. Este apresenta uma visão geral da área através de análise e categorização de evidências. O estudo idenfitica gaps, tendências, e provê direções futuras para pesquisa. Ademais, esta dissertação trata do fenômeno de bad smells de arquitetura no contexto de LPSs através de dois estudos exploratórios em domínios diferentes. O primeiro estudo exploratório conduz uma investigação sobre as implicações de propriedades estruturais em uma LPS no domínio de editores de texto, enquanto o segundo estudo foca em uma LPS no domínio mobile. Antes da busca pelos smells em ambos os estudos, informações relevantes para a arquitetura foram recuperadas do código fonte para que as arquiteturas fossem definidas.

Made available in DSpace on 2016-06-02T19:05:37Z (GMT). No. of bitstreams: 1 2316.pdf: 4618889 bytes, checksum: d562a70baf332d9b2ca5ed3f42ec15e2 (MD5) Previous issue date: 2008-09-11 / Research in sensor networks is widely regarded both as one of the most challenging and prospering area. Matching Computer Science concepts with Electrical Engineer applicability, Wireless Sensor and Actors Networks (WSAN) can be used to develop several case studies in manner to build applications which will be useful for evolving the WSAN s architecture, infra-structure and its components in general. Due to technologies advances reached by these scientific researches, the processing unities became exponentially more powerful with smaller size and lower cost, enabling the widespread use of the WSAN and making this technology more popular. So, it is clear that applications which depend on the WSAN s infrastructure to build system, in several applications domains, have been emerging. Actually, there are applications ranging from habitat monitoring to military purposes. One of the major problems associated with WSAN is the difficulty of developing software applications. Recent researches has shown that service oriented programming models may contribute to improve communication and interoperability between heterogeneous devices in pervasive spaces. Organizations seeking to develop WSAN applications can obtain a competitive advantage by developing applications on an architecture which supports reusability, maintainability and extendibility. Therefore, this work proposes the use of a service oriented approach for the development and management of applications specialized in remote area surveillance based on wireless and sensor networks characteristics and concepts. / A pesquisa em redes de sensores é considerada uma das áreas que mais apresenta desafios e com maior potencial para crescimento. Ao combinar a teoria e conceitos da Ciência da Computação com a aplicabilidade da Engenharia Elétrica, as Redes de Sensores e Atuadores Sem Fio (RSASF) apresentam uma enorme variedade de estudos de casos para o desenvolvimento de aplicações que auxiliam na evolução da arquitetura, infraestrutura e dos componentes em geral dessas redes. Devido aos avanços tecnológicos resultantes dessas pesquisas cientificas, as unidades de processamento tornaram-se exponencialmente mais poderosas, de menor tamanho físico e com menor custo financeiro, impulsionando a utilização das RSASF e tornando-as cada vez mais populares. Desse modo, é evidente o surgimento de aplicações que utilizam ao menos algum dos conceitos e características inerentes às RSASF como infraestrutura para o desenvolvimento de sistemas nos mais variados domínios de aplicação. Atualmente, existem aplicações dos conceitos das RSASF desde monitoramento ambiental até utilização em campo militar. Um dos maiores problemas associados à RSASF está na dificuldade do desenvolvimento de aplicações para estas redes, derivados do fato da existência de grande heterogeneidade de dispositivos e a falta de padronização de codificação. Pesquisas recentes têm demonstrado que modelos de programação orientados a serviços podem contribuir para melhorar a comunicação e interoperabilidade entre esses dispositivos heterogêneos. O desenvolvimento de aplicações para estas redes provê vantagens competitivas com o uso de Arquiteturas Orientadas a Serviços (SOA Service-oriented Architecture) ao desenvolver aplicações em uma arquitetura que suporta reusabilidade, manutenção facilitada, gerenciamento e estensibilidade. Dessa forma, este trabalho propõe o uso de uma abordagem orientada a serviços para o desenvolvimento e gerenciamento de aplicações com fins de atuação e monitoramento que utilizam conceitos e características das RSASF.

Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-05-08T17:28:24Z No. of bitstreams: 1 IZABELA VANESSA DE ALMEIDA MELO - DISSERTAÇÃO PPGCC 2015..pdf: 3198472 bytes, checksum: 824f30587ab3b750011a08d2e5d6019a (MD5) / Made available in DSpace on 2018-05-08T17:28:24Z (GMT). No. of bitstreams: 1 IZABELA VANESSA DE ALMEIDA MELO - DISSERTAÇÃO PPGCC 2015..pdf: 3198472 bytes, checksum: 824f30587ab3b750011a08d2e5d6019a (MD5) Previous issue date: 2015-09-10 / Desde os anos 90 a comunidade científica desempenha esforços para estudar e evoluir aspectos relacionados à Arquitetura de Software, aumentando seu volume de publicação a partir de 1999. O aumento significativo das publicações nos últimos anos demonstra a importância e preocupação que a academia tem com relação a essa área. Porém, a partir da troca de experiência entre pesquisadores e profissionais da área, percebe-se que a indústria não parece conhecer/utilizar o que é proposto pela academia. O contexto teórico sobre arquitetura de software, documentação arquitetural e verificação de conformidade arquitetural já é conhecido no meio acadêmico. Porém, qual é o contexto deles dentro da indústria? Como os profissionais definem o termo "arquitetura desoftware"? Como os profissionais realizam (se realizam) a documentação arquitetural? Como realizam (se realizam) a verificação de conformidade arquitetural? O que eles pensam sobre ferramentas de apoio à verificação de conformidade arquitetural? Para responder essas questões, realizamos um estudo qualitativo dividido em 3 etapas. Primeiro, aplicamos um survey exploratório com o objetivo de entender o ambiente prático para ter uma noção sobre o contexto em foco. Enviamos o questionário para 149 profissionais e 4 grupos de discussão, obtendo uma taxa de resposta de 24,1%. Na segunda etapa entrevistamos 14 profissionais voluntários que responderam o survey exploratório (taxa de resposta de 40%). O objetivo desta etapa foi nos aprofundarmos no contexto em foco. Por fim, nossa última etapa consistiu de um survey confirmatório. Enviamos o questionário para os usuários do GitHub que possuem endereços de e-mail visíveis e tem mais de 100 seguidores (obtivemos uma taxa de resposta de 7,74%). Como resultados principais, observamos que não há uma única definição para o termo "arquitetura de software", dependendo de fatores desde a experiência do profissional até a empresa em que trabalham. Além disso, existem documentações arquiteturais, mas, a sua maioria não é rigorosa, formal e não é atualizada. Nem todos realizam verificação de conformidade arquitetural, e, quando realizam, normalmente é feita de forma manual. Os principais motivos para a não documentação e/ou verificação são falta de tempo ou falta de necessidade. Porfim, as ferramentas de apoio à verificação de conformidade arquitetural não são muito utilizadas e/ou conhecidas. / Since the 90’s a big effort has been applied in the academy to study and evolve aspects related to Software Architecture, increasing the amount of publications from 1999 to the present-day. The significant rise in the number of publications in the last few years shows how much importance and concern academia gives to this particular area. However, after discussing what has been experienced by researchers and professionals of this area, it is possible to notice that the industry does not know/use what is proposed in the academy. The theoretical context about software architecture, architectural documentation and architectural conformance checking is already known. However, what about the practical/industrial context? How do the professionals define “software architecture”? How do they document (if they do) the architecture? How do they perform (if they do) architectural conformance checking? What do they think about support tools for architectural conformance checking? Aiming to answer these questions, we performed a 3-step qualitative study. Firstly, we applied an exploratory survey with the goal of understanding the practical environment and having a better notion about the context of our study. We sent the survey to 149 professionals and 4 discussion groups, getting 24.1% of response rate. In the second phase we interviewed 14 volunteered professionals who responded the exploratory survey (response rate of 40%). In this phase we wanted to deeply understand the context of your study. Finally, the last phase consisted of a confirmatory survey which goal was to confirm our findings. We sent the survey to GitHub users with public e-mails and more than 100 followers, getting 7.74% of response rate. As main results we observed that there is not a single definition of“software architecture” and that it depends on several factors, as the professional’s experience and the company in which he/she works. The architecture is sometimes documented but, most of the time, the documentation is incomplete, informal and outdated. In many cases, architectural conformance checking is not performed or it is performed manually. The main reasons for not documenting or verifying the architecture are lack of time and/or need. Finally, the support tools for architectural conformance checking are not often used and not well known.

Embora o conceito de reuso não seja novo em engenharia de software, a conscientização sobre sua importância e seu impacto no desenvolvimento de sistemas computacionais ainda não é generalizada. Uma das principais dificuldades encontradas pelas empresas de desenvolvimento é a inexistência de métodos efetivos para reuso de software. As pesquisas em engenharia de software que enfocam o reuso de software têm gerado contribuições crescentes na forma de paradigmas (como a orientação a objeto), de conceitos (como domínios e componentes) e de métodos e processos. Mais recentemente, o conceito de Padrão (Pattern) possibilitou novas formas de representações e a proposição de métodos ainda mais orientados ao reuso. Os padrões de software denominados padrões de projeto e padrões de programação (ou idiomas) têm sido bem explorados na literatura científica. Modelos de representação e exemplos são encontrados em artigos e livros especializados. O conceito de Padrão Arquitetural, entretanto, não possui a mesma maturidade. Trata-se de um conceito mais abrangente envolvendo modelos e técnicas mais extensos e complexos. Essencialmente, um Padrão Arquitetural é um modelo genérico de uma solução de software para um determinado domínio. Seu desenvolvimento permite que se possa reusar toda a arquitetura de um sistema em novos projetos semelhantes. O objetivo deste trabalho é oferecer uma contribuição para uma metodologia de identificação e descrição de Padrões Arquiteturais de Software. Para atingir este objetivo foram criadas cinco tipologias para serem empregadas como extensão da UML na descrição de casos de uso, classes, seqüências, estados e componentes. Esta descrição diferenciada visa evidenciar, nos diagramas da UML, as partes do padrão que são variantes, opcionais e múltiplas. Estas tipologias são empregadas no metamodelo desenvolvido para a descrição dos padrões arquiteturais. A utilização do metamodelo e, conseqüentemente, das tipologias é guiada pelos passos de um processo que também foi criado para servir como um roteiro para se chegar à descrição do padrão arquitetural. / Although the concept of reuse is not new in software engineering, the awareness of its importance and its impact in the development of computational systems is not generalized yet. One of the main difficulties found by development companies is the absence of effective methods for software reuse. The researches on software engineering that focuses software reuse have generated increasing contributions in the form of paradigms (such as object orientation), concepts (such as domain and component), and methods, languages and processes. More recently, the concept of Pattern allowed new representation forms and the proposal of methods even more reuse-oriented. Software patterns named as Design Patterns and Programming Patterns (or Idioms) have been well explored at scientific literature. Representation models and examples related to these patterns type are found in articles and specialized books. The concept of Architectural Pattern, however, does not have the same maturity. This is a more including concept involving more extensive and complex models and techniques. Essentially, an Architectural Pattern is a generic model of a software solution to a determined domain. Its development may allow the reuse of all the architecture of a system in new similar projects. This work aims to offer a contribution for a methodology of Software Architectural Patterns identification and description. In order to achieve this objective, five typologies have been created to be employed as UML extension in the description of use cases, classes, sequences, states and components. This differentiated description aims to evidence, in the UML diagrams, variant, optional, and multiple pattern parts. These typologies are used in the developed metamodel for the architectural patterns description. The use of the metamodel, and consequently the use of typologies, is guided by the steps of a process, which was also created to serve as a guideline to accomplish the architectural pattern description.

Embora o conceito de reuso não seja novo em engenharia de software, a conscientização sobre sua importância e seu impacto no desenvolvimento de sistemas computacionais ainda não é generalizada. Uma das principais dificuldades encontradas pelas empresas de desenvolvimento é a inexistência de métodos efetivos para reuso de software. As pesquisas em engenharia de software que enfocam o reuso de software têm gerado contribuições crescentes na forma de paradigmas (como a orientação a objeto), de conceitos (como domínios e componentes) e de métodos e processos. Mais recentemente, o conceito de Padrão (Pattern) possibilitou novas formas de representações e a proposição de métodos ainda mais orientados ao reuso. Os padrões de software denominados padrões de projeto e padrões de programação (ou idiomas) têm sido bem explorados na literatura científica. Modelos de representação e exemplos são encontrados em artigos e livros especializados. O conceito de Padrão Arquitetural, entretanto, não possui a mesma maturidade. Trata-se de um conceito mais abrangente envolvendo modelos e técnicas mais extensos e complexos. Essencialmente, um Padrão Arquitetural é um modelo genérico de uma solução de software para um determinado domínio. Seu desenvolvimento permite que se possa reusar toda a arquitetura de um sistema em novos projetos semelhantes. O objetivo deste trabalho é oferecer uma contribuição para uma metodologia de identificação e descrição de Padrões Arquiteturais de Software. Para atingir este objetivo foram criadas cinco tipologias para serem empregadas como extensão da UML na descrição de casos de uso, classes, seqüências, estados e componentes. Esta descrição diferenciada visa evidenciar, nos diagramas da UML, as partes do padrão que são variantes, opcionais e múltiplas. Estas tipologias são empregadas no metamodelo desenvolvido para a descrição dos padrões arquiteturais. A utilização do metamodelo e, conseqüentemente, das tipologias é guiada pelos passos de um processo que também foi criado para servir como um roteiro para se chegar à descrição do padrão arquitetural. / Although the concept of reuse is not new in software engineering, the awareness of its importance and its impact in the development of computational systems is not generalized yet. One of the main difficulties found by development companies is the absence of effective methods for software reuse. The researches on software engineering that focuses software reuse have generated increasing contributions in the form of paradigms (such as object orientation), concepts (such as domain and component), and methods, languages and processes. More recently, the concept of Pattern allowed new representation forms and the proposal of methods even more reuse-oriented. Software patterns named as Design Patterns and Programming Patterns (or Idioms) have been well explored at scientific literature. Representation models and examples related to these patterns type are found in articles and specialized books. The concept of Architectural Pattern, however, does not have the same maturity. This is a more including concept involving more extensive and complex models and techniques. Essentially, an Architectural Pattern is a generic model of a software solution to a determined domain. Its development may allow the reuse of all the architecture of a system in new similar projects. This work aims to offer a contribution for a methodology of Software Architectural Patterns identification and description. In order to achieve this objective, five typologies have been created to be employed as UML extension in the description of use cases, classes, sequences, states and components. This differentiated description aims to evidence, in the UML diagrams, variant, optional, and multiple pattern parts. These typologies are used in the developed metamodel for the architectural patterns description. The use of the metamodel, and consequently the use of typologies, is guided by the steps of a process, which was also created to serve as a guideline to accomplish the architectural pattern description.

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.

Embedded systems, including critical embedded systems (CES) are increasingly present in the modern society, providing specific solutions from small to large complex systems, such as in cars, airplanes, and healthcare equipment. Failures in these systems can result in damage to human beings, and to the environment, or can represent an unrecoverable financial loss. In this sense, it is very important to ensure they are built with quality. To provide such quality, it is necessary to consider their software architecture, which impacts on the quality of the systems. This way, the main objective of this Masters project is to propose a quality model concerning the most important quality attributes for CES, which may be used to support (but not limited to) architectural activities such as analysis and evaluation in the context of CES. / Sistemas embarcados, incluindo sistemas embarcados críticos (SEC), estão cada vez mais presentes na sociedade moderna, provendo soluções específicas que variam de sistemas pequenos até sistemas grandes e complexos, como é possível encontrar em carros, aviões e equipamentos médicos. Falhas nesses sistemas podem resultar em danos à seres humanos e ao meio ambiente, ou então em uma perda financeira irrecuperável. Sendo assim, é muito importante garantir que os SEC sejam construídos e apresentem um nível adequado de qualidade. Para garantir que esses sistemas alcancem tal qualidade, é necessário considerar sua arquitetura de software, já que esta impacta de maneira significativa na qualidade do software enquanto artefato ou produto. Deste modo, o objetivo deste projeto de mestrado é de propor um modelo de qualidade que contém os atributos de qualidade mais importantes para SEC, servindo como artefato para apoiar a execução de atividades arquiteturais (além de outras que possam se beneficiar) tais como análise e avaliação, no contexto de SEC.