State Compression In SPIN: State-vector Optimization Based On Property

Model checking is an important approach which guarantees program correctness, with the benefit that it is completely automatic. However, its application to even larger and more complex systems is limited by the so-called state space explosion problem: for many types of systems, the number of possible states during system execution grows exponentially with the size of the system and the number of its component parts. This quickly leads to models whose size exceeds the current capabilities of verification tools.SPIN is a popular open-source software tool that can be used for the formal verification of distributed software systems. SPIN adopts the partial order reduction strategy to reduce the number of system states that needs to be visited and stored in the state space to solve the model checking problem. An orthogonal strategy is to reduce the amount of memory that is required to store each system state. This is the domain of memory compression techniques.This thesis presents a kind of lossless compression technique for SPIN named state-vector optimization based on property, or SOBP for short, it makes use of the characteristics of system property, optimizes state-vector by substituting two or more variables in property with one variable, thus achieves state-vector compression. Moreover, when SOBP combined with collapse compression, it will make collapse compression stronger, consequently reducing the amount of memory further. Similar to other lossless compression techniques in SPIN, SOBP increases the run-time requirements while reduces the memory requirements of an exhaustive search.