On Memory-Block Traversal Problems in Model Checking Timed Systems

A major problem in model-checking timed systems is thehuge memory requirement. In this paper, we study the memory-blocktraversal problems of using standard operating systems in exploring thestate-space of timed automata. We report a case study which demonstratesthat deallocating memory blocks (i.e. memory-block traversal)using standard memory management routines is extremely time-consuming.The phenomenon is demonstrated in a number of experiments byinstalling the Uppaal tool on Windows95, SunOS 5 and Linux. It seemsthat the problem should be solved by implementing a memory managerfor the model-checker, which is a troublesome task as it is involved inthe underlining hardware and operating system. We present an alternativetechnique that allows the model-checker to control the memory-blocktraversal strategies of the operating systems without implementingan independent memory manager. The technique is implemented in theUppaal model-checker. Our experiments demonstrate that it results insignificant improvement on the performance of Uppaal. For example, itreduces the memory deallocation time in checking a start-up synchronisationprotocol on Linux from 7 days to about 1 hour. We show that thetechnique can also be applied in speeding up re-traversals of exploredstate-space