| Campo DC | Valor | Idioma |
|---|
| dc.contributor.advisor | Alves, Vander Ramos | - |
| dc.contributor.author | Castro, Thiago Mael de | - |
| dc.date.accessioned | 2020-07-09T13:41:37Z | - |
| dc.date.available | 2020-07-09T13:41:37Z | - |
| dc.date.issued | 2020-07-09 | - |
| dc.date.submitted | 2019-12-13 | - |
| dc.identifier.citation | CASTRO, Thiago Mael de. A Machine-Verified Theory of commuting strategies for product-line reliability analysis. 2019. 208 f., il. Tese (Doutorado em Informática)—Universidade de Brasília, Brasília, 2019. | pt_BR |
| dc.identifier.uri | https://repositorio.unb.br/handle/10482/39241 | - |
| dc.description | Tese (doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2019. | pt_BR |
| dc.description.abstract | Engenharia de linha de produtos de software é uma forma de gerenciar
sistematicamente a variabilidade e a comunalidade em sistemas de software,
possibilitando a síntese automática de programas relacionados (produtos) a partir de
um conjunto de artefatos reutilizáveis. No entanto, o número de produtos em uma linha
de produtos de software pode crescer exponencialmente em função de seu número de
características. Mesmo linhas de produtos com dezenas ou centenas de opções de
configuração (features) podem dar origem a milhões de produtos, tornando inviável
verificar a qualidade de cada um desses produtos isoladamente. Não obstante, linhas
de produtos de software crítico (por exemplo, nos domínios de aviação e sistemas
médicos) necessitam garantir que seus produtos são confiáveis.
Existem diversas abordagens cientes de variabilidade para análise de linha de
produtos, as quais adaptam técnicas de análise de produtos isolados para lidar com
variabilidade de forma eficiente. Tais abordagens podem ser classificadas em três
dimensões combináveis de análise (product-based, family-based e feature-based),
mas, particularmente no contexto de análise de confiabilidade, não existe uma teoria
que compreenda (a) uma especificação formal das três dimensões e das estratégias de
análise resultantes e (b) prova de que tais análises são equivalentes umas às outras. A
falta de uma teoria com essas propriedades dificulta que se raciocine formalmente
sobre o relacionamento entre as dimensões de análise e técnicas de análise derivadas.
Além disso, a falta de evidência de que as diferentes estratégias são mutuamente
equivalentes limita os resultados desses estudos empíricos existentes.
Para ajudar a preencher essa lacuna, formalizamos sete abordagens para
análise de confiabilidade em linhas de produtos, cobrindo todas as três dimensões de
análise e incluindo a primeira instância de análise feature-family-product-based na
literatura. Provamos que as estratégias formalizadas são corretas em relação à
abordagem para análise de confiabilidade de produtos individuais, fortalecendo as
comparações empíricas entre elas. Desse modo, engenheiros podem escolher a
estratégia mais apropriada à linha de produtos em questão, seguros de sua corretude.
Adicionalmente, apresentamos um diagrama comutativo de passos
intermediários de análise, o qual relaciona estratégias diferentes e permite reusar
demonstrações de corretude entre elas. Essa visão contribui para uma compreensão
mais abrangente sobre os princípios subjacentes às estratégias, o que visualiza-se
poder ajudar outros pesquisadores a alçar técnicas de análise de software para
abordagens cientes de variabilidade ainda inexploradas.
Além disso, reduzimos o risco de erro humano por meio da mecanização da
teoria resultante no provador interativo de teoremas chamado PVS (Prototype
Verification System). Como resultado do esforço de mecanização, identificamos erros e
imprecisões na versão manualmente especificada de nossa teoria, os quais foram
consequentemente corrigidos. Portanto, documentamos as lições aprendidas com o
esforço de mecanização e apresentamos uma teoria verificada por máquina
potencialmente reutilizável. | pt_BR |
| dc.language.iso | Inglês | pt_BR |
| dc.rights | Acesso Aberto | pt_BR |
| dc.title | A Machine-Verified Theory of commuting strategies for product-line reliability analysis | pt_BR |
| dc.type | Tese | pt_BR |
| dc.subject.keyword | Linha de produto de software | pt_BR |
| dc.subject.keyword | Análise de confiabilidade | pt_BR |
| dc.subject.keyword | Model checking | pt_BR |
| dc.subject.keyword | Verificação formal | pt_BR |
| dc.rights.license | A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor com as seguintes condições: Na qualidade de titular dos direitos de autor da publicação, autorizo a Universidade de Brasília e o IBICT a disponibilizar por meio dos sites www.bce.unb.br, www.ibict.br, http://hercules.vtls.com/cgi-bin/ndltd/chameleon?lng=pt&skin=ndltd sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra disponibilizada, conforme permissões assinaladas, para fins de leitura, impressão e/ou download, a título de divulgação da produção científica brasileira, a partir desta data. | pt_BR |
| dc.description.abstract1 | Software product line engineering is a means to systematically manage variability
and commonality in software systems, enabling the automated synthesis of related
programs (products) from a set of reusable assets. However, the number of products in
a software product line may grow exponentially with the number of features, so it is
practically infeasible to quality-check each of these products in isolation. Nonetheless,
product lines of safety-critical software (e.g., in the domains of avionics and medical
systems) need to ensure that its products are reliable.
There are a number of variability-aware approaches to product-line analysis that
adapt single-product analysis techniques to cope with variability in an efficient way.
Such approaches can be classified along three composable analysis dimensions
(product-based, family-based, and feature-based), but, particularly in the context of
reliability analysis, there is no theory comprising both (a) a formal specification of the
three dimensions and resulting analysis strategies and (b) proof that such analyses are
equivalent to one another. The lack of such a theory hinders formal reasoning on the
relationship between the analysis dimensions and derived analysis techniques.
Moreover, as long as there is no evidence that the different examined strategies are
mutually equivalent, the existing empirical studies comparing them will have limited
results.
To address this issue, we formalize seven approaches to user-oriented reliability
analysis of product lines, covering all three analysis dimensions and including the first
instance of a feature-family-product-based analysis in the literature. We prove the
formalized analysis strategies to be sound with respect to reliability analysis of a single
product, thereby strengthening the existing empirical comparison between them.
Furthermore, we present a commuting diagram of intermediate analysis steps,
which relates different strategies and enables the reuse of soundness proofs between
them. Such view contributes to a more comprehensive understanding of underlying
principles used in these strategies, which we envision could help other researchers to
lift existing single-product analysis techniques to yet under-explored variability-aware
approaches.
Additionally, we reduce the risk of human error by mechanizing the resulting
theory in the PVS interactive theorem prover. As a result, we identified and corrected
errors and imprecisions of the handcrafted version. Hence, we document lessons
learned throughout the mechanization process and provide a potentially reusable
machine-verified theory. | pt_BR |
| dc.description.unidade | Instituto de Ciências Exatas (IE) | pt_BR |
| dc.description.unidade | Departamento de Ciência da Computação (IE CIC) | pt_BR |
| dc.description.ppg | Programa de Pós-Graduação em Informática | pt_BR |
| Aparece nas coleções: | Teses, dissertações e produtos pós-doutorado
|
