00 CAMPUS ARISTÓTELES CALAZANS SIMÕES (CAMPUS A. C. SIMÕES) IC - INSTITUTO DE COMPUTAÇÃO Dissertações e Teses defendidas na UFAL - IC
Use este identificador para citar ou linkar para este item: http://www.repositorio.ufal.br/jspui/handle/riufal/1540
Tipo: Dissertação
Título: Um método para verificação formal e dinâmica de sistemas de software concorrentes
Título(s) alternativo(s): A method for formal and dynamic verification of concurrent software systems
Autor(es): Santos, Bruno Roberto
Primeiro Orientador: Silva, Leandro Dias da
metadata.dc.contributor.advisor-co1: Ribeiro, Márcio de Medeiros
metadata.dc.contributor.referee1: Brito, Patrick Henrique da Silva
metadata.dc.contributor.referee2: Perkusich, Angelo
Resumo: Neste trabalho é apresentado um método para verificação formal e dinâmica de software concorrentes. O objetivo é oferecer um método capaz de identificar problemas inerentes a programas cuja execução baseia-se em múltiplas threads, além de analisar propriedades comportamentais descritas com base nos preceitos da lógica temporal. Propõe-se um método capaz de detectar problemas e verificar formalmente a adequação da execução de sistemas de software concorrentes com relação ao comportamento desejável a tais sistemas, baseando-se em informações coletadas dinamicamente, ou seja, em tempo de execução. As informações coletadas correspondem às sequências de execução de sistemas de software, bem como dados sobre a maneira como se comunicam seus componentes durante sua execução. Os dados colhidos refletem a execução do sistema de software propriamente dito, o que garante maior confiança às informações coletadas. Tais informações são analisadas de modo a identificar impasses e condições de corrida em um processo denominado Análise Dinâmica. Ademais, estas informações também são utilizadas para geração automática de um modelo que descreve o comportamento do sistema de software, o qual é utilizado para verificação de propriedades comportamentais. A este processo de verificação dá-se o nome de Verificação Formal. A geração automática do modelo elimina a necessidade de construção manual do mesmo, que requer muito esforço e conhecimento acerca de métodos formais, isso pode aumentar custos e tempo de desenvolvimento do sistema de software. Entretanto, a análise dinâmica é conhecida por apenas realizar cobertura sobre o comportamento atual de sistemas de software concorrentes, sem considerar a análise de todas as outras possíveis sequências de execuções devido ao não determinismo. Em razão do comportamento não determinístico, sistemas de software concorrentes são capazes de produzir resultados diferentes para a mesma entrada a cada nova execução. Deste modo, reproduzir o comportamento que leva sistemas de software concorrente à falha é uma tarefa complexa. O presente trabalho propõe um método para realizar verificação formal e dinâmica de sistemas de software concorrente capaz de capturar o comportamento não determinístico desses sistemas, além de proporcionar a redução de custos de desenvolvimento através da eliminação da necessidade de construção manual de modelos de sistemas de software concorrente. O método é validado através de um estudo de caso composto por testes em três sistemas de software.
Abstract: This work presents a method to perform formal and dynamic verification of concurrent software. The objective is to provide a method capable of identifying problems in programs whose execution is based on multiple threads, and analyze behavioral properties. The method is able to detect problems in concurrent software, as well as check conformity of the concurrent software with desirable behavior, based on information collected dynamically, i.e. at runtime. The information collected consists of the software execution flow as well as data about the way communicate the software components during this run. The data collected reflect the software's execution, which ensures greater confidence to the information collected. This information is analyzed to identify deadlocks and race conditions in a process called Dynamic Analysis. In addition, this information is also used to automatically generate a model that describes the behavior of a software, which is used for verification of behavioral properties. This process is called Formal Verification. The automatic model generation eliminates the need for manual construction of the model, which requires much effort and knowledge of formal methods, this can increase costs and development time software. However, the dynamic analysis is known to only perform coverage of the current behavior of competing software systems. Current behavior is one that occurs only during an execution of concurrent software systems, without considering all other possible behaviors from the non-determinism. Due to the non-determinism, concurrent software can produce different results for the same input to each execution of software. Therefore reproduce the behavior that leads to competitive software failure is a complex task. This paper proposes a method to perform formal verification and dynamic concurrent software capable of capturing the non-deterministic behavior of these systems and provide reduced development costs by eliminating the need for manual construction of concurrent software system models. The method is validated by a case study consists of three test software systems.
Palavras-chave: Verificação formal
Sistemas concorrentes
Análise dinâmica
Formal verification
Concurrent systems
Dynamic analysis
CNPq: CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO
Idioma: por
País: Brasil
Editor: Universidade Federal de Alagoas
Sigla da Instituição: UFAL
metadata.dc.publisher.program: Programa de Pós-Graduação em Modelagem Computacional de Conhecimento
Citação: SANTOS, Bruno Roberto. Um método para verificação formal e dinâmica de sistemas de software concorrentes. 2016. 77 f. Dissertação (Mestrado em Modelagem Computacional de Conhecimento) – Instituto de Computação, Programa Pós Graduação em Modelagem Computacional de Conhecimento, Universidade Federal de Alagoas, Maceió, 2016.
Tipo de Acesso: Acesso Aberto
URI: http://www.repositorio.ufal.br/handle/riufal/1540
Data do documento: 20-mai-2016
Aparece nas coleções:Dissertações e Teses defendidas na UFAL - IC

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
Um método para verificação formal e dinâmica de sistemas .pdf1.97 MBAdobe PDFVisualizar/Abrir


Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.