Skip to main content
Erschienen in:
Buchtitelbild

1999 | OriginalPaper | Buchkapitel

Runtime Efficient State Compaction in Spin

verfasst von : J Geldenhuys, P J A de Villiers, John Rushby

Erschienen in: Theoretical and Practical Aspects of SPIN Model Checking

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Metadaten
Titel
Runtime Efficient State Compaction in Spin
verfasst von
J Geldenhuys
P J A de Villiers
John Rushby
Copyright-Jahr
1999
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/3-540-48234-2_2