Making the right cut in model checking data-intensive timed systems

摘要: The success of industrial-scale model checkers such as UPPAAL [3] or NUSMV [12] relies on the efficiency their respective symbolic state space representations. While difference bound matrices (DBMs) are effective for representing sets clock values, binary decision diagrams (BDDs) can efficiently represent huge discrete sets. In this paper, we introduce a simple general framework combining both data structures, enabling joint representation timed in reachability fixed point construction. contrast to other approaches, our technique is robust against intricate interdependencies between constraints and location information. Especially analysis models with only few clocks, large constants, (such as, e.g., data-intensive communication protocols), turns out be highly effective. Additionally, allows employ existing highly-optimized implementations DBMs BDDs without modifications. Using prototype implementation, able verify central correctness property physical layer protocol FlexRay [15] taking an unreliable into account.