|
On Memory-Block Traversal Problems in Model Checking Timed Systems
Fredrik Larsson
January 2000 |
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
Available as PostScript, PDF, DVI. |