1999 | OriginalPaper | Chapter
Runtime Efficient State Compaction in Spin
Authors : J Geldenhuys, P J A de Villiers, John Rushby
Published in: Theoretical and Practical Aspects of SPIN Model Checking
Publisher: Springer Berlin Heidelberg
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Spin is a verification system that can detect errors automatically by exploring the reachable state space of a system. The efficiency of verifiers like Spin depends crucially on the technique used for the representation of states. A number of recent proposals for more compact representations reduce the memory requirements, but cause a considerable increase in execution time. These methods could be used as alternatives when the standard state representation exhausts the memory, but this is exactly when the additional overhead is least affordable.We describe a simple but effective state representation scheme that can be used in conjunction with Spin’s normal modes of operation. We compare the idea to Spin’s standard state representation and describe how Spin was modified to support it. Experimental results show that the technique provides a valuable reduction in memory requirements and simultaneously reduce the execution time. For the cases considered an average reduction in memory requirements of 40% was measured and execution time was reduced on average by 19%. The proposed technique could therefore be considered to replace the default technique in Spin.