Memory Efficient State-Space Analysis in Software Model-Checking

Mukherjee, A., Tari, Z. and Bertok, P.

Formal methods have an unprecedented ability to endorse the correctness of a system. In spite of that, it has been limited to safety-critical and mission-critical systems owing to significant time and memory costs involved. Lately, our ever increasing dependency on software in all walks of our life has necessitated using formal methods for a wider range of softwares. In this paper, we propose an algorithm to make this possible by reducing the memory requirement for model checking, a widely used formal method. A model- checker stores all explored states in memory to ensure termination. The proposed algorithm slash memory costs by storing these states in compressed form. In compressed form, a state is stored as how different it is from its previous state. Our experiments report a memory reduction of 95% with only doubling of computation delay. Aforesaid reduction allows model checking in a machine with only a fraction of memory needed otherwise. Consequently the advantage is twofold, 1) enormous savings as only a small physical memory is required and 2) as more states can now be stored in a memory of same size, the chances of complete state-space analysis is exceedingly high.

Cite as: Mukherjee, A., Tari, Z. and Bertok, P. (2010). Memory Efficient State-Space Analysis in Software Model-Checking. In Proc. 33rd Australasian Computer Science Conference (ACSC 2010) Brisbane, Australia. CRPIT, 102. Mans, B. and Reynolds, M. Eds., ACS. 23-32

(from crpit.com) (local if available)