Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-15T15:01:06Z No. of bitstreams: 1 AMANDA SARAIVA BEZERRA - DISSERTAÇÃO PPGCC 2008..pdf: 5823735 bytes, checksum: 68f742006dbac9f251bc1a10ef99a69a (MD5) / Made available in DSpace on 2018-08-15T15:01:06Z (GMT). No. of bitstreams: 1 AMANDA SARAIVA BEZERRA - DISSERTAÇÃO PPGCC 2008..pdf: 5823735 bytes, checksum: 68f742006dbac9f251bc1a10ef99a69a (MD5) Previous issue date: 2008-11-28 / Capes / Verificar o comportamento de Sistemas Distribuídos é difícil. Algumas técnicas, como Model Checking, tentam garantir a corretude comportamental de um sistema analisando todos os seus caminhos de execução. Entretanto, esta técnica é limitada para a análise de sistemas consideravelmente pequenos. A técnica de Design by Contract (DbC) sugere a construção de um conjunto de asserções que devem ser verificadas em tempo de execução. Estas asserções são checagens instantâneas, podendo estas serem atendidas ou violadas. Como DbC não dá suporte à verificação de asserções temporais, cuja checagem deve ser realizadas sobre vários instantes,então construímos uma técnica que possibilita a verificação comportamental de Sistemas Distribuídos, verificando se a execução apresentada está de acordo com os requisitos comportamentais definidos para o sistema. Inicialmente é necessário definir os requisitos, que devem descrever o comportamento desejado para o sistema. Como estes requisitos devem ser checagens contínuas utilizamos a Lógica Temporal Linear (LTL) para descrever a evolução do comportamento ao longo do tempo. Usamos então LTL para definir o conjunto de propriedades comportamentais especificadas para o sistema distribuído implementado em Java. Cada propriedade comportamental deve ser verificada sobre um conjunto específico de objetos do sistema, são os chamados pontos de interesse. Este pontos têm relação direta e devem obedecer a uma determinada propriedade comportamental. Durante a execução é realizada a captura de informações dos pontos de interesse a serem analisados, esta captura é feita usando a Programação Orientada a Aspectos (POA). A linguagem AspectJ, implementação de POA, possibilita a captura de informações sem a necessidade de modificar o código fonte do sistema a ser analisado. Durante a execução do sistema é realizada a monitoração, além da captura da informação, sendo necessária uma ordenação parcial dos eventos provocados pelos processos que compõem o sistema distribuído. A ordenação é feita com base na relação de causa e efeito entre os eventos, assim usamos o conceito de Relógios Lógicos, que possibilita uma ordenação parcial dos eventos gerados durante a execução do sistema. Após a captura e organização dos eventos, é realizada a verificação comportamental apresentada pelos eventos de acordo com o conjunto de propriedades definidas para tal. Se em algum momento desta verificação alguma propriedade for violada, então dizemos que foi encontrado um comportamento inesperado ou anômalo, de acordo com o especificado. Esta violação é apresentada para o desenvolvedor ou testador do sistema, que tomará as devidas providências para localizar e corrigir a violação detectada. Como prova de conceito, implementamos a ferramenta DistributedDesignMonitor (DDM), realizando a monitoração de Sistemas Distribuídos implementados na linguagem Java. O DDM é apresentado e discutido através de experimentos realizados com a ferramenta, mostrando como fazer uso da técnica de monitoração. / Verify Distributed Systems is very hard. Some techniques, Model Checking for example, trying to grant the behavioral correctness analyzing all the execution paths for these systems. However, this technique is limited to check small systems. The Design by Contract technique (DbC) suggests makes a set of assertions that should be verified at runtime. These assertions are instant checks, which could be satisfied or violated. As DbC does not support the verification of temporal assertions, which check should be done over a lot of instant time for the execution, so we built a technique that verifies the Distributed Systems' behavior, verifying if the system execution is in accordance with the behavior requirements for it Initially is necessary the requirement definition, which should describe the desired system behavior. These requirements should be continuous checks, so we use the Linear Temporal Logic (LTL) to describe the evolution of the behavior over the time. The LTL is used to define set of behavioral properties specified for a Java Distributed System. Each behavioral property should be verified over defined objects of the system, they are the points of interest. These points should obey to the behavioral property defined for them. During the execution the information catch of each point of interest is done by the Aspect Oriented Programming (AOP). The language AspecU makes possible the capture of runtime information without intrusiveness. During the system execution starts the monitoring, being necessary a partial order of the events of the distributed system processes. The ordering is done based on the relation of cause and effect between events, so we use the Logical Clocks to do this partial order. After the capture and the organization of the events, the behavioral verification is done in accordance with the specified properties defined for this system. If some violation was detected during the system verification, so we found an inconsistent or unexpected behavior, in accordance with the specification. This violation is showed to the system developer or tester, which will correct the analyzed system. In this work we implemented the DistributedDesignMonitor (DDM) tool to prove our concept, monitoring Distributed Systems implemented in Java language. O DDM is presented and discussed using experiments, showed how use the monitoring technique