Synchronous Closing and Flow Analysis for Model Checking Timed Systems

The paper develops the idea that modal logic provides an appropriate framework for the specification of data flow analysis (DFA) algorithms as soon as programs are represented as models of the logic. This can be exploited to construct a DFA-generator that generates efficient DFA-algorithms from modal specifications by partially evaluating a specific model checker wrt the specifying modal formula. Moreover, the use of a modal logic as specification language for DFA-algorithms supports the compositional development of specifications and structured proofs of properties of DFA-algorithms. These ideas are applied to the problem of determining optimal computation points within flow graphs.

Download Full-text

On Memory-Block Traversal Problems in Model Checking Timed Systems

BRICS Report Series ◽

10.7146/brics.v7i3.20131 ◽

2000 ◽

Vol 7 (3) ◽

Author(s):

Fredrik Larsson ◽

Paul Pettersson ◽

Wang Yi

Keyword(s):

Model Checking ◽

State Space ◽

Operating Systems ◽

Memory Management ◽

Timed Automata ◽

Model Checker ◽

Timed Systems ◽

Memory Block ◽

Start Up

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.

Download Full-text

Data-Flow Analysis as Model Checking Within the jABC

Lecture Notes in Computer Science - Compiler Construction ◽

10.1007/11688839_9 ◽

2006 ◽

pp. 101-104 ◽

Cited By ~ 8

Author(s):

Anna-Lena Lamprecht ◽

Tiziana Margaria ◽

Bernhard Steffen

Keyword(s):

Model Checking ◽

Data Flow ◽

Flow Analysis ◽

Data Flow Analysis

Download Full-text