A Machine-Verified Theory of commuting strategies for product-line reliability analysis

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.