Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems
Farn Wang
¡@
A new data-structure called DDD (Data-Decision Diagram) for the fully
symbolic model-checking of real-time software systems is proposed.
DDD is a BDD-like structure for the encoding of regions. Unlike DBM
which records differences between pairs of clock readings, DDD only
uses one auxiliary binary variable for each clock. Thus the number of
variables used in DDD is always linear to the number of clocks declared
in the input system description. Experiment has been carried out to
compare
DDD with previous technologies.