Return to search

Detecção automática de violações de propriedades de sistemas concorrentes em tempo de execução. / Automatic detection of competing system property violations at run time.

Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-22T19:52:23Z
No. of bitstreams: 1
ANA EMÍLIA VICTOR BARBOSA - DISSERTAÇÃO PPGCC 2007..pdf: 1669761 bytes, checksum: f47054507fe9200c8d1d56d2848ae276 (MD5) / Made available in DSpace on 2018-08-22T19:52:23Z (GMT). No. of bitstreams: 1
ANA EMÍLIA VICTOR BARBOSA - DISSERTAÇÃO PPGCC 2007..pdf: 1669761 bytes, checksum: f47054507fe9200c8d1d56d2848ae276 (MD5)
Previous issue date: 2007-04-20 / Capes / Neste trabalho propomos uma técnica que visa detectar violações de propriedades comportamentais automaticamente durante a execução de sistema de software concorrentes. A técnica foi inspirada na metodologia de desenvolvimento Design by Contract (DbC). DbC permite que os desenvolvedores adicionem aos programas asserções para que sejam verificadas em tempo de execução. O uso de asserções para expressar propriedades de programas concorrentes (multithreaded)eparalelos,
entretanto,não ésuficiente. Nesses sistemas,muitas das propriedades
comportamentais de interesse, como vivacidade e segurança, não podem ser expressas apenas com asserções. Essas propriedades requerem o uso de operadores temporais. Neste trabalho, utilizamos Lógica Linear Temporal (Linear Time Logic - LTL) para expressar o comportamento desejado. Para dar suporte a checagem do comportamento dos programas em tempo de execução,
propomos uma técnica baseada em Programação Orientada a Aspectos, que permite que
o programa seja continuamente monitorado (o comportamento é checado através do uso
de autômatos que permite a deteção de comportamentos inesperados). Associada a cada
propriedade comportamental existe um conjunto de pontos de interesse do código-fonte que devem obedece-la. Esses pontos são então monitorados durante a execução do sistema através do uso de aspectos. Entre outros benefícios, a técnica permite que o sistema de software alvo seja instrumentado de maneira não intrusiva, sem alterar o código-fonte — particulamente, nenhum código do software alvo deve ser modificado para execução da monitoração. Para validar este trabalho, desenvolvemos como prova de conceitos um protótipo que implementa a técnica e permite a monitoração de programas Java multi-threaded, chamado DesignMonitor. Essa ferramenta é apresentada e discutida através de um estudo de caso para demonstrar a aplicação da técnica / In this work we propose and develop a technique that allows to detect the violation of
behavior properties of concurrent systems. The technique was inspired by the Design by
Contract (DbC) programming methodology, which proposes the use of assertions and their
evaluation at runtime to check programs behavior. The use of simple assertions to express properties of concurrent and parallel programs, however, is not sufficient. Many of the relevant properties of those systems,s uch as liveness and security, can not be expressed with simple assertions. Thesepropertiesrequiretheuseof temporal operators. In our work, we used Linear Time Logic (LTL) to specify the expected behavior. To support the runtime checking of the program against the expected behavior, we propose a technique, based on Aspect-Oriented Programming, that allows the program to be continuously monitored (behavior is checked against automata that allows the detection of unexpected behaviors). Each property is mapped to a set of points of interest in the target
program. Those points are then monitored during the system execution through aspects.
Among other benefits, the technique allows the instrumentation of the target software to
be performed automatically and in a non-intrusive way — in particular, no code must be
changed toturn monitoring on or off. To validate the work, we developed a proof of concept prototype tool that implements the technique and allows the monitoring of multi-threaded Java programs, called DesignMonitor. The tool was used in case study that has allowed the evaluation and the discussion of practical issues related with the technique.

Identiferoai:union.ndltd.org:IBICT/oai:localhost:riufcg/1532
Date22 August 2018
CreatorsBARBOSA, Ana Emília Victor.
ContributorsGUERRERO, Dalton Dario Serey., FIGUEIREDO, Jorge César Abrantes de., MACHADO, Patrícia Duarte de Lima., SIMÃO, Adenilso da Silva.
PublisherUniversidade Federal de Campina Grande, PÓS-GRADUAÇÃO EM CIÊNCIA DA COMPUTAÇÃO, UFCG, Brasil, Centro de Engenharia Elétrica e Informática - CEEI
Source SetsIBICT Brazilian ETDs
LanguagePortuguese
Detected LanguageEnglish
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis
Sourcereponame:Biblioteca de Teses e Dissertações da UFCG, instname:Universidade Federal de Campina Grande, instacron:UFCG
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0107 seconds