Efficient Memory Deallocation Techniques in Real-Time Model-Checking

During the past few years, a number of software tools for automated analysis of real-time systems have been developed in the framework of timed automata (e.g. Kronos and Uppaal). One of the major problems in applying these tools to industrial-size systems is the huge memory-usage for state-space exploration as the model-checkers must keep track of the clock values of the automata, specified by clock constraints. The huge memory requirement often results in swapping, which is time-consuming. Thus the part of state-space explored, that is not needed for further analysis during the verification process should be thrown away whenever possible to reduce swapping. This in turn requires memory deallocation operations. As the first contribution of this paper, we report a case study on memory allocation and deallocation behaviour of verification tools for real time systems. We discovered that deallocating memory blocks during state-space exploration using standard memory management routines in..