Making the Right Cut in Model Checking Data-Intensive Timed Systems
Rüdiger Ehlers, Michael Gerke, and Hans-Jörg Peter
The success of industrial-scale model checkers such as Uppaal or NuSMV relies on the efficiency of their respective symbolic state space representations. While difference bound matrices (DBMs) are effective for representing sets of clock values, binary decision diagrams (BDDs) can efficiently represent huge discrete state sets. In this paper, we introduce a simple general framework for combining both data structures, enabling a joint symbolic representation of the timed state sets in the reachability fixed point construction. In contrast to other approaches, our technique is neither sensitive to the magnitude of the clocks nor suffers from intricate interdependencies between clock constraints and the location information. Especially in the analysis of models with only few clocks, large constants, and a huge discrete state space (such as, e.g., data-intensive communication protocols), our technique turns out to be highly effective. Additionally, our framework allows to employ existing highly- optimized implementations for DBMs and BDDs without modifications. Using a prototype implementation, we are able to verify a central correctness property of the coding/decoding part of the FlexRay communication protocol taking an unreliable physical layer into account.
12th International Conference on Formal Engineering Methods (ICFEM 2010).
Copyright by Springer Verlag. The original publication is available at www.springerlink.com.