Verification of symmetric models using semiautomatic abstractions

Abstract

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.