Verification of Hierarchical State/Event Systems using Reusability and Compositionality

by Gerd Behrmann, Kim G. Larsen. Henrik Reif Andersen, Henrik Hulgaard and Jørn Lind-Nielsen.

In TACAS'99: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Springer.

Abstract

We investigate techniques for verifying hierarchical systems, i.e., finite state systems with a nesting capability. The straightforward way of analysing a hierarchical system is to first flatten it into an equivalent non-hierarchical system and then apply existing finite state system verification techniques. Though conceptually simple, flattening is severely punished by the hierarchical depth of a system. To alleviate this problem, we develop a technique that exploits the hierarchical structure to reuse earlier reachability checks of superstates to conclude reachability of substates. We combine the reusability technique with the successful compositional technique of [1] and investigate the combination experimentally on industrial systems and hierarchical systems generated according to our expectations to real systems. The experimental results are very encouraging: whereas a flattening approach degrades in performance with an increase in the hierarchical depth (even when applying the technique of [1]), the new approach proves not only insensitive to the hierarchical depth, but even leads to improved performance as the depth increases.

[BiBTeX entry] [Postscript]