Symbolic Reachability Graph Generation for High-level Models based on Synthesized Operators

Abstract

This paper introduces a new technique for generating Binary Decision Diagrams (BDDs) representing high-level model’s underlying state/tran- sition systems. The obtained decision diagram may serve as input for various analysis methods such as symbolic (probabilistic) model checking and/or Markovian performance and reliability analysis. As usual the pro- posed technique makes use of partitioned symbolic reachability analysis. However, contrary to existing techniques it neither relies on pregenerated symbolic representations of transition relations, nor does it make use ofstandard BDD-manipulating algorithms. Instead, symbolic reachability analysis is carried out by means of customized BDD-algorithms directly synthesized from high-level models to be analyzed. Overall the presentedapproach yields the core of a new tool bench for the symbolic analysis of state-based system descriptions. The tool bench is implemented on topof the Eclipse Modeling Framework and exploits Java Emitter Templates for code synthesis. Standard benchmark models show that for generating high-level models underlying state/transition systems significant improve- ments with respect to CPU time and memory consumption can be real- ized, ultimately allowing the verification of larger and much more complex systems.