Local livelock analysis of component-based models

The use of increasingly complex applications is demanding a greater investment of resources in software development to ensure that applications are safe. For mastering this complexity, compositional approaches can be used in the development of software by integrating and reusing existing reliable...

ver descrição completa

Na minha lista:
Detalhes bibliográficos
Autor principal: Conserva Filho, Madiel de Souza
Outros Autores: Oliveira, Marcel Vinicius Medeiros
Formato: doctoralThesis
Idioma:por
Publicado em: Brasil
Assuntos:
Desenvolvimento baseado em componentes
Métodos formais
Ausência de livelock
Análise local
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
Endereço do item:https://repositorio.ufrn.br/jspui/handle/123456789/22209
Tags: Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
id ri-123456789-22209
record_format dspace
institution Repositório Institucional
collection RI - UFRN
language por
topic Desenvolvimento baseado em componentes
Métodos formais
Ausência de livelock
Análise local
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
spellingShingle Desenvolvimento baseado em componentes
Métodos formais
Ausência de livelock
Análise local
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
Conserva Filho, Madiel de Souza
Local livelock analysis of component-based models
description The use of increasingly complex applications is demanding a greater investment of resources in software development to ensure that applications are safe. For mastering this complexity, compositional approaches can be used in the development of software by integrating and reusing existing reliable components. The correct application of such strategies, however, relies on the trust in the behaviour of the components and in the emergent behaviour of the composed components because failures may arise if the composition does not preserve essential properties. Problems may be introduced when two or more error-free components are integrated for the first time. This concern is even more relevant when a group of components is put together in order to perform certain tasks, especially in safety-critical applications, during which classical problems can arise, such as livelock. In this thesis, we present a local strategy that guarantees, by construction, the absence of livelock in synchronous systems as modelled using the standard CSP notation. Our method is based solely on the local analysis of the minimum sequences that lead the CSP model back to its initial state. Locality provides an alternative to circumvent the state explosion generated by the interaction of components and allows us to identify livelock before composition. The verification of these conditions use metadata that allow us to record partial results of verification, decreasing the overall analysis effort. In addition, our work can also be applied to check livelock freedom in models that perform asynchronous communications. In this case, we carry out livelock analysis in the context of a component model, BR IC, whose behaviour of the components is described as a CSP process. Finally, we introduce three case studies to evaluate our livelock analysis technique in practice: the Milner’s scheduler and two variations of the dining philosophers, a livelock-free version and a version in which we have deliberately included livelock. For each case study, we also present a comparative analysis of the performance of our strategy with two other techniques for livelock freedom verification, the traditional global analysis of FDR and the static livelock analysis of SLAP. This comparative study demonstrates that our strategy can be used in practice and that it might be a useful alternative for establishing livelock freedom in large systems.
author2 Oliveira, Marcel Vinicius Medeiros
author_facet Oliveira, Marcel Vinicius Medeiros
Conserva Filho, Madiel de Souza
format doctoralThesis
author Conserva Filho, Madiel de Souza
author_sort Conserva Filho, Madiel de Souza
title Local livelock analysis of component-based models
title_short Local livelock analysis of component-based models
title_full Local livelock analysis of component-based models
title_fullStr Local livelock analysis of component-based models
title_full_unstemmed Local livelock analysis of component-based models
title_sort local livelock analysis of component-based models
publisher Brasil
publishDate 2017
url https://repositorio.ufrn.br/jspui/handle/123456789/22209
work_keys_str_mv AT conservafilhomadieldesouza locallivelockanalysisofcomponentbasedmodels
_version_ 1773963499193499648
spelling ri-123456789-222092017-11-04T02:29:53Z Local livelock analysis of component-based models Conserva Filho, Madiel de Souza Oliveira, Marcel Vinicius Medeiros http://lattes.cnpq.br/1756952696097255 Cavalcanti, Ana Lucia Caneca Mota, Alexandre Cabral http://lattes.cnpq.br/2794026545404598 Moreira, Anamaria Martins http://lattes.cnpq.br/2363575151206774 Ribeiro, Leila Musicante, Martin Alejandro http://lattes.cnpq.br/6034405930958244 Desenvolvimento baseado em componentes Métodos formais Ausência de livelock Análise local CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO The use of increasingly complex applications is demanding a greater investment of resources in software development to ensure that applications are safe. For mastering this complexity, compositional approaches can be used in the development of software by integrating and reusing existing reliable components. The correct application of such strategies, however, relies on the trust in the behaviour of the components and in the emergent behaviour of the composed components because failures may arise if the composition does not preserve essential properties. Problems may be introduced when two or more error-free components are integrated for the first time. This concern is even more relevant when a group of components is put together in order to perform certain tasks, especially in safety-critical applications, during which classical problems can arise, such as livelock. In this thesis, we present a local strategy that guarantees, by construction, the absence of livelock in synchronous systems as modelled using the standard CSP notation. Our method is based solely on the local analysis of the minimum sequences that lead the CSP model back to its initial state. Locality provides an alternative to circumvent the state explosion generated by the interaction of components and allows us to identify livelock before composition. The verification of these conditions use metadata that allow us to record partial results of verification, decreasing the overall analysis effort. In addition, our work can also be applied to check livelock freedom in models that perform asynchronous communications. In this case, we carry out livelock analysis in the context of a component model, BR IC, whose behaviour of the components is described as a CSP process. Finally, we introduce three case studies to evaluate our livelock analysis technique in practice: the Milner’s scheduler and two variations of the dining philosophers, a livelock-free version and a version in which we have deliberately included livelock. For each case study, we also present a comparative analysis of the performance of our strategy with two other techniques for livelock freedom verification, the traditional global analysis of FDR and the static livelock analysis of SLAP. This comparative study demonstrates that our strategy can be used in practice and that it might be a useful alternative for establishing livelock freedom in large systems. O uso crescente de sistemas complexos exige cada vez mais um maior investimento de recursos no desenvolvimento de software para garantir a confiabilidade dos mesmos. Para lidar com esta complexidade, abordagens composicionais podem ser utilizadas no desenvolvimento de sistemas de software, possibilitando a integração e a reutilização de componentes existentes. Entretanto, a fim de garantir o sucesso desta abordagem, é essencial confiar no comportamento dos componentes e, além disso, nos sistemas que são desenvolvidos utilizando essa estratégia, uma vez que falhas podem ser introduzidas se a composição não assegurar propriedades importantes. Problemas podem surgir quando dois ou mais componentes são integrados pela primeira vez. Esta situação é ainda mais relevante quando um grupo de componentes trabalha em conjunto a fim de executar determinadas tarefas, especialmente em aplicações críticas, onde podem surgir problemas clássicos, como livelock. Esta tese de doutorado apresenta uma estratégia local para garantir ausência de livelock, por construção, em sistemas síncronos modelados com a notação padrão de CSP. A nossa técnica é baseada na análise local das mínimas sequências que levam o processo CSP ao seu estado inicial. O uso de técnicas locais evita a explosão do espaço de estados gerado pela integração dos componentes. A verificação destas condições locais utilizam metadados que permitem armazenar resultados parciais das verificações, reduzindo o esforço durante a análise. A abordagem proposta também pode ser aplicada para verificar ausência de livelock em modelos que realizam comunicações assíncronas. Neste caso, analisamos o modelo de componentes BR IC, cujo comportamento dos componentes é representado por um processo CSP. A fim de realizar esta verificação, consideramos duas versões para BR IC: BR IC , o qual realiza composições assíncronas através de buffers finitos, e BR IC¥ no qual a assincronicidade é realizada através de buffers infinitos. Estas duas abordagens foram analisadas porque a possibilidade de introduzir livelock em sistemas assíncronos depende diretamente da finitude do buffer. As técnicas propostas para garantir ausência de livelock em CSP e BR IC foram avaliadas através de três estudos de caso: o escalonador de Milner e duas variações do jantar dos filósofos. Uma versão apresenta um sistema livre de livelock, e a outra apresenta um sistema com livelock. Neste estudo, avaliamos a nossa abordagem em comparação com outras duas técnicas para verificação de ausência de livelock, a análise global tradicional do FDR e a análise estática de livelock do SLAP. Este estudo comparativo demonstra que a nossa estratégia pode ser aplicada como uma alternativa para a verificação de ausência de livelock em grandes sistemas. 2017-03-10T21:13:38Z 2017-03-10T21:13:38Z 2016-08-12 doctoralThesis CONSERVA FILHO, Madiel de Souza. Local livelock analysis of component-based models. 2016. 150f. Tese (Doutorado em Ciência da Computação) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2016. https://repositorio.ufrn.br/jspui/handle/123456789/22209 por Acesso Aberto application/pdf Brasil UFRN PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO

Registros relacionados