On Memory-Block Traversal Problems in Model Checking Timed Systems

Abstract

A major problem in model-checking timed systems is the
huge memory requirement. In this paper, we study the memory-block
traversal problems of using standard operating systems in exploring the
state-space of timed automata. We report a case study which demonstrates
that 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 by
installing the Uppaal tool on Windows95, SunOS 5 and Linux. It seems
that the problem should be solved by implementing a memory manager
for the model-checker, which is a troublesome task as it is involved in
the underlining hardware and operating system. We present an alternative
technique that allows the model-checker to control the memory-block
traversal strategies of the operating systems without implementing
an independent memory manager. The technique is implemented in the
Uppaal model-checker. Our experiments demonstrate that it results in
significant improvement on the performance of Uppaal. For example, it
reduces the memory deallocation time in checking a start-up synchronisation
protocol on Linux from 7 days to about 1 hour. We show that the
technique can also be applied in speeding up re-traversals of explored
state-space.