Verification of symmetric models using semiautomatic abstractions

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.Model Checking is a powerful method for the formal verification of concurrent systems. It explores automatically the state-space of a model that represents the system to prove its correctness in relation to formal specifications, which are described using some temporal logic. Despite its importance and wide application, Model Checking suffers with the state-space explosion: the number of states of a model is exponential to its size; thus it limits the size of the models that may be verified. Many techniques were proposed to overcome this problem. Among them, the use of abstractions is considered one of the most general and efficient. The adoption of abstractions consists of generating a reduced model from the original model by merging or removing states that are irrelevant to the specification being verified. Another technique is the symmetry reduction. It is based on the observation that several models present some level of symmetry, and states considered equivalent can be grouped. Thus, the state-space to be considered is significantly smaller and the exploration of only one of the states of the same group is sufficient to prove the correctness of some propriety. This work combines both techniques to produce reduced models that can be verified at feasible time. It presents a methodology to generate semiautomatic abstractions, based on the model symmetry. The key idea is that, for the verification of certain proprieties, the removal of symmetric components of a model has a small impact on information loss caused by the abstractions since its symmetric counterpart is still represented. The methodology defines modeling premises to make the abstractionadoption semiautomatic, i.e., without the need to alter the model description. Moreover, it presents abstraction patterns based on the system symmetry and shows which specifications are consistent with each pattern. The techniques presented in this work are specially useful on the verification of computation systems that present considerable replication of structures. This characteristic can be observed in memories, caches, bus protocols, multi-processes applicationsand network protocols. In this work the model of a P2P Live Streaming application was implemented to validate the methodology. At this model each participant receives and forwards data to its partners to reconstruct the original live stream. The fact that all peers are distinct processes that share the same code makes this model highly symmetric and thus a valid example. The reductions obtained by the methodology proved to be very significant. I.e, the calculation of the number of reachable states of the original model, from a total of approximately 273 possible states, has not finished after more than two weeks of intensive computation. In contrast, the same computation for the reduced models finished in less than two minutes in all cases and the maximum number of reachablestates found was approximately 219