Verification of symmetric models using semiautomatic abstractions
Pedro de Carvalho Gomes · Americanae (AECID Library) · 2010
A Verificação de Modelos é uma técnica poderosa de verificação automática de sistemas concorrentes. Ela explora automaticamente os estados de um modelo que representa o sistema para provar sua correção com relação a especificações formais, descritas usandoalguma lógica temporal. Apesar de sua importância e ampla aplicação, a Verificação de Modelos sofre com o problema da explosão de estados: o número de estados do modelo é exponencial ao seu tamanho; isto limita o tamanho dos modelos possíveis de serem verificados.Diversas técnicas foram propostas para contornar o problema. Dentre elas, o uso de abstrações é considerada uma das mais genéricas e eficientes. A adoção de abstrações consiste em gerar um modelo reduzido a partir do modelo original através da fusão ou remoção de estados que supõe-se irrelevantes com relação à propriedadesendo verificada. Outra técnica é a redução por simetria. Ela baseia-se na observação que diversos sistemas apresentam considerável grau de simetria, e estados considerados equivalentes podem ser agrupados. Assim o espaço dos estados a ser considerado é significantemente menor e a exploração de apenas um dos estados do mesmo grupo ésuficiente para provar a correção de alguma propriedade. Este trabalho combina ambas as técnicas para produzir modelos reduzidos, quepodem ser verificados em tempo factível. É apresentada uma metodologia para gerar abstrações semiautomáticas, baseada na simetria do modelo. A ideia chave é que, na verificação de certas propriedades, a remoção de componentes simétricos de ummodelo tem um impacto pequeno na perda de informação causada pelas abstrações já que a contra-parte simétrica ainda está presente. A metodologia define premissas de modelagem para tornar a adoção das abstrações semiautomática, ou seja, sem a necessidade de alterar a descrição do modelo. Além disso, são apresentados padrõesde abstrações baseados na simetria do sistema e mostra-se quais especificações são consistentes com cada padrão. As técnicas apresentadas neste trabalho são especialmente úteis na verificaçãode sistemas de computação que apresentam uma considerável replicação de estrutura. Tal característica pode ser observada em memórias, caches, protocolos de barramento, programas com vários processos e protocolos de rede. Foi implementado no trabalhoo modelo de uma rede P2P Live Streaming para validar a metodologia. Neste modelo cada participante recebe e encaminha dados para seus parceiros para reconstruir o conteúdo ao vivo original. O fato de todos os participantes serem processos distintos que compartilham o mesmo código torna este modelo altamente simétrico e assim umexemplo válido. A redução obtida com a metodologia provou ser bastante significativa. Por exemplo, o cálculo do número de estados alcançáveis do modelo original, de um total de aproximadamente 273 estados possíveis, não terminou após mais de duas semanasde computação intensa. Em contrapartida, a mesma computação para os modelos reduzidos terminou em menos de três minutos em todos os casos e o número máximo encontrado de estados alcançáveis foi de aproximadamente 219.