Disk Based Model Checking Disk Based Model Checking

by Bao, Tonglaga 1977-

Abstract (Summary)

Disk based model checking does not receive much attention in the model checking field becasue of its costly time overhead. In this thesis, we present a new disk based algorithm that can get close to or faster verification speed than a RAM based algorithm that has enough memory to complete its verification. This algorithm also outperforms Stern and Dill's original disk based algorithm. The algorithm partitions the state space to several files, and swaps files into and out of memory during verification. Compared with the RAM only algorithm, the new algoritm reduces hash table insertion time by reducing the cost and growth of the hash load. Compared with Stern's disk based algorithm, the new disk based algorithm significantly reduces disk vs memory comparsion but increases disk read/write time. The size of the model the new algorithm can verify is bound to the available disk size instead of the available RAM size.

Bibliographical Information:


School:Brigham Young University

School Location:USA - Utah

Source Type:Master's Thesis

Keywords:model checking disk


Date of Publication:10/11/2004

© 2009 All Rights Reserved.