Uma técnica de análise de conformidade comportamental para sistemas distribuídos. - BEZERRA, Amanda Saraiva. (2008)
Veriﬁcar 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 veriﬁcadas 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 à veriﬁcação de asserções temporais, cuja checagem deve ser realizadas sobre vários instantes,então construímos uma técnica que possibilita a veriﬁcação comportamental de Sistemas Distribuídos, veriﬁcando se a execução apresentada está de acordo com os requisitos comportamentais deﬁnidos para o sistema. Inicialmente é necessário deﬁnir 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 deﬁnir o conjunto de propriedades comportamentais especiﬁcadas para o sistema distribuído implementado em Java. Cada propriedade comportamental deve ser veriﬁcada sobre um conjunto especíﬁco 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 modiﬁcar 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 veriﬁcação comportamental apresentada pelos eventos de acordo com o conjunto de propriedades deﬁnidas para tal. Se em algum momento desta veriﬁcação alguma propriedade for violada, então dizemos que foi encontrado um comportamento inesperado ou anômalo, de acordo com o especiﬁcado. 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.