Making the Right Cut in Model Checking Data-Intensive Timed Systems

Abstract. The success of industrial-scale model checkers such as Uppaal [3] or NuSMV [12] 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 robust against 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 implementati...

• Type: Journal
• Year: 2010
• Where: ICFEM
• Authors: Rüdiger Ehlers, Michael Gerke 0002, Hans-Jörg Peter
• Keywords: Huge Discrete State, ICFEM 2010, Software Engineering, State Sets, State Space