Estágio realizado na Siemens, S. A. e orientado pelo Eng.º António Martins / Tese de mestrado integrado. Engenharia Informática e Computação. Faculdade de Engenharia. Universidade do Porto. 2008

Tese de mestrado. Redes e Serviços de Comunicação. Faculdade de Engenharia. Universidade do Porto. 2006

Made available in DSpace on 2013-08-07T18:42:49Z (GMT). No. of bitstreams: 1 000444044-Texto+Completo-0.pdf: 1517934 bytes, checksum: 017ad238277ccab4a746e7590ed0bade (MD5) Previous issue date: 2012 / The development of distributed systems and communication protocols is not a trivial task and the use of formal specification and verification techniques becomes necessary to assure the correctness of such systems. While model-checking techniques face the state space explosion problem, the use of theorem provers is an important resource for verification of systems with unlimited number of states. The formal method Event-B, increasingly being used in both industry and academia, is based on the technique of theorem proving and also supports refinement. The contribution of this work is a library of reusable formal specification patterns, in Event-B, for message passing mechanisms commonly employed in distributed systems. A specification pattern defines the desired communication semantics of a channel, having its properties formally proven. During the development of a distributed system, the developer may use these patterns by applying guided refinement steps on the target model. The resulting system is assured to have the communication semantics as defined by the pattern, thus freeing the developer of defining the communication system from scratch and of proving its properties. / O desenvolvimento de sistemas distribuídos e protocolos de comunicação é uma tarefa complexa e o uso de técnicas de especificação e verificação formal torna-se necessário para garantir a corretude de tais sistemas. Enquanto técnicas de model-checking passam pelo problema da explosão do espaço de estados, o uso de provadores de teoremas representa um importante recurso para verificação de sistemas com ilimitado número estados. O método formal Event-B, de uso crescente na indústria e academia, se apóia na técnica de prova de teoremas e suporta refinamento. A contribuição deste trabalho está em proporcionar uma biblioteca reusável de padrões de especificação, em Event-B, de mecanismos de troca de mensagens em sistemas distribuídos. Um padrão de especificação define a semântica de comunicação desejada em um canal, demostrando formalmente suas propriedades. Durante o desenvolvimento de um sistema distribuído, o desenvolvedor pode fazer uso destes padrões através de passos guiados de refinamento do sistema. O sistema resultante garante a semantica de comunicação definida no padrão utilizado e livra o desenvolvedor de se preocupar em definir o sistema de comunicação a partir do início e provar suas propriedades.

Made available in DSpace on 2013-08-07T18:43:36Z (GMT). No. of bitstreams: 1 000423774-Texto+Completo-0.pdf: 1356397 bytes, checksum: 4c07d8d5aba7d673efbc82c220109747 (MD5) Previous issue date: 2007 / This work’s main goal is the research of protocols for ad hoc network formation, targeting the modeling of a scheme for building a new Bluetooth scatternet protocol. This protocol has as its main feature to be compliant with the requirements of interactive applications, which are more dependent on a better connection availability than on large bandwidth with low communication delay. The modeled protocol keeps the connection up, even in the events of nodes going in and out the mobile network. The protocol has been proposed targeting a Bluetooth SoC implementation for scatternet formation. Initially, the validation strategy had been conceived targeting the IP´s Fˆenix Platform. A simulation was performed in order to obtain experimental data from the proposed model for scatternet´s generation. / Este trabalho tem como principal objetivo a investigação de protocolos para formação de redes ad hoc, visando a modelagem de novo protocolo para formação de scatternets Bluetooth. Esse protocolo tem por característica principal atender os requisitos de aplicações interativas, que dependem mais de uma maior disponibilidade da conexão do que de uma conexão com largura de banda elevada e com baixo atraso de comunicação. O protocolo modelado mantém conexões funcionando mesmo na presença de eventos de entrada e saída de nós da rede móvel. O protocolo foi proposto visando a implementação de um SoC Bluetooth para a formação de scatternets. A validação inicialmente foi idealizada para utilização da plataforma Fênix do projeto Brazil IP, sendo ao final realizada uma simulação para levantamento de resultados do modelo para geração de scatternets.

Made available in DSpace on 2019-03-29T23:23:01Z (GMT). No. of bitstreams: 0 Previous issue date: 2010-03-16 / A mobile replicated database is comprised of several devices dynamically distributed, interconnected through a wireless network with intermittent connectivity, where there are multiple copies the same database stored in database servers (replicas), distributed throughout the network. The use of data replication in mobile computing environments increases data availability and throughtput of transactions. In order to ensure data consistency in mobile replicated databases, several replication control protocols have been proposed. However, most of them reveal relevant limitations, such as: possessing a single failure point and flooding the network with messages exchange. In this work is introduced a protocol which guarantees data consistency of replicated databases in mobile computing. The proposed approach is completely distributed, avoids the existence of a single failure point, uses a read-any/write-any replication scheme, increases data availability, and reduces the number of messages exchanged among the replicated servers. Furthermore, it allows the user to choose a transaction isolation level (degree in which the execution of a given transaction is isolated from all other concurrent transactions). Experimental results show the potential efficiency of the proposed approach. Keywords: Concurrency Control, Data Replication, Mobile Computing / Um banco de dados móvel replicado é composto por diversos dispositivos distribuídos de forma dinâmica (servidores e/ou clientes), interconectados através de uma rede sem fio com conectividade intermitente, onde existem várias cópias de um mesmo banco de dados armazenadas em servidores de banco e dados conhecidos como réplicas, distribuídos pela rede. O uso da replicação de dados em ambientes de computação móvel possibilita o aumento da disponibilidade dos dados e da vazão das transações. A fim de garantir a consistência de dados em banco de dados móveis replicados, vários protocolos de controle de réplica têm sido propostos. Entretanto, a maioria deles possui limitações relevantes, tais como: possuir um ponto único de falha ou sobrecarregar a rede com intensa troca de mensagens. Neste trabalho de dissertação é proposto um protocolo que garante consistência de bancos de dados replicados em ambiente de computação móvel. A abordagem proposta é completamente distribuída, evitando a ocorrência de um ponto único de falha, utiliza o esquema de replicação read-any/write-any, aumentando a disponibilidade dos dados, e pode reduzir o número de mensagens trocadas entre os servidores replicados. Além disso, permite ao usuário escolher o nível de isolamento de transação (grau em que a execução de uma determinada transação é isolada das outras transações concorrentes). Experimentos realizados em um simulador, com análise de desempenho comparativa, comprovam a eficiência da abordagem proposta. Palavras-chaves: Controle de Concorrência, Replicação de Dados, Computação Móvel

Tese de mestrado integrado. Engenharia Electrotécnica e de Computadores (Major Automação). Faculdade de Engenharia. Universidade do Porto. 2010

Made available in DSpace on 2014-06-12T15:59:09Z (GMT). No. of bitstreams: 2 arquivo4916_1.pdf: 1434670 bytes, checksum: abaa8d06582fc44f7e90eb4168cc59c9 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2004 / Fundação de Amparo à Pesquisa do Estado do Amazonas / O uso de técnicas de simulação para implementar cenários de testes em protocolos de comunicação tem crescido bastante nos últimos anos. Centros de pesquisas acadêmicos e industriais têm dedicado especial interesse em simulação de ambientes com variados graus de complexidade, sobretudo pelo baixo custo e pela rapidez com que os experimentos podem ser implementados, corrigidos, aplicados e reproduzidos em comparação com um ambiente real de operação. Apesar disso, as técnicas de simulação inerentemente envolvem alto nível de abstração na modelagem e mapeamento dos cenários, o que pode comprometer a representatividade e confiabilidade dos resultados obtidos. O arcabouço de testes de conformidade proposto pela ITU-T/ISO através das recomendações OSI-9646 tem sido amplamente utilizado pela indústria de telecomunicações na certificação de seus produtos. Esse arcabouço abrange todas as fases do desenvolvimento dos testes de conformidade, desde planejamento, derivação e implementação do conjunto de testes até a fase de aplicação e análise dos resultados dos testes. O propósito fundamental dos testes de conformidade é verificar se uma implementação se comporta de modo consistente em relação às suas especificações, proporcionando dessa maneira um mecanismo para aumentar o grau de interoperabilidade entre produtos certificados de fabricantes distintos. Para a descrição dos testes, foi definida a linguagem TTCN – Testing and Test Control Notation, cuja característica abstrata permite que um conjunto de testes possa ser integrado a diversas implementações de um mesmo protocolo. Em sua terceira versão, essa linguagem também permite a descrição e implementação de testes de performance e de robustez. Este trabalho propõe adaptar o arcabouço de testes de conformidade como um método de validação de protocolos de comunicação em ambientes de simulação, considerando os aspectos relevantes da modelagem abstrata e permitindo o mapeamento de não-conformidade no cenário de simulação antes da realização dos experimentos, dessa forma, possibilitando aumentar a confiabilidade dos cenários utilizados em simulações de protocolos de comunicação

Existe uma demanda crescente na indústria aeronáutica por redes de comunicação baseadas em barramentos bidirecionais e capazes de lidar com um maior volume de tráfego produzido pelos modernos sistemas aviônicos, para substituir os padrões antigos, a exemplo do ARINC 429. Estas novas redes devem oferecer confiabilidade e segurança compatíveis com sistemas embarcados distintos, com níveis de criticalidade diferentes, e em grande integração. Por outro lado, há uma preocupação das autoridades certificadoras de aviação em definir normas aplicáveis à integração dessas tecnologias em desenvolvimento aos novos projetos. Neste trabalho, a evolução destas tecnologias é brevemente apresentada e são discutidas as principais características de alguns padrões industriais para redes recentemente disponíveis no mercado: FlexRay, TTP/C, ARINC 629 e AFDX. Esta discussão é orientada por critérios que estão relacionados a segurança e desempenho, conforme as considerações da AC 20-156, publicada pelo FAA em 2006. Desenvolve-se uma análise de risco funcional, e são discutidas algumas hipóteses de falha. São também apresentados conceitos de determinismo e influência do overhead sobre protocolos de comunicação.

Os sistemas de suporte a trabalho cooperativo tem se mostrado, nos ultimos cinco anos, uma solucao para problemas de comunicacao e coordenacao em atividades que envolvem grupos de pessoas. Este trabalho apresenta uma analise historica da evolucao de tais sistemas, define conceitos atraves da discussao de algumas taxonomias, discute alguns elementos da Teoria da Coordenacao, descreve experiencias anteriores na utilizacao de tais sistemas e, a partir disso, propoe um conjunto de caracteristicas a serem consideradas no projeto de tais sistemas. Um sistema de suporte a trabalho cooperativo, chamado MULTIMAIL, e especificado ate o nivel de projeto. O sistema MULTIMAIL e voltado a automatizacao de varias atividades que envolvem comunicacao e coordenacao entre grupos de pessoas em uma organizacao tipica do setor de servicos. Um prototipo, chamado PROMAIL, e implementado com base no projeto do sistema MULTIMAIL. O projeto do sistema MULTIMAIL propoe a incorporacao, em sua interface, de recursos hipermidia e é inteiramente baseado no paradigma dos sistemas de correio eletronicoEste projeto e feito atraves de uma abordagem de analise de projeto orientado a objetos.

Service Oriented Architecture (SOA) allows the development of software with requirements of interoperability and loose coupling. New services can be offered through the composition of existing services in order to address new business requirements. Business-to-business collaborative web applications demand a loosely coupled, coarse-grained interaction model. Thus, the traditional transaction architectures based on the ACID must be re-visited to support long-running web services. For such web services, it is not advisable to lock resources because they become blocked to other transactions. The two most adopted SOA architecture styles are the WS-* and REST (Representational State Transfer). WS-* is a set of specifications for the development of services based on SOAP and WSDL. The WS-* specifications support the implementation of non-functional requirements among them the transaction control. Two of the WS-* drawbacks are the implementation complexity and the strong dependency on SOAP and WSDL. REST, however, as an architectural style, does not provide "official" standards to address the non-functional requirements of services. We investigate the means by which a web service application can support transactions implementation using timestamp. We propose a protocol based in timestamp and two phase commit protocol in order to support the transactional control implementation in the web service domain. A protocol extension to improve the satisfaction of business rules is also proposed. The extension takes into account the application domain business rules which guide the web services behavior. In order to show the feasibility of the protocols, examples of an application are described. We also describe how the proposed protocols must be used to deal with host and connection failures.