Efficient data structure for fully symbolic verification of real-time software systems

Abstract

A new data-structure called RED(Region-Encoding Diagram) for the fully symbolic model-checking of real-time software systems is proposed. RED is a BDD-like data-structure for the encoding of regions [2]. Unlike DBM which records differences between pairs of clock readings, REDonly uses one auxiliary binary variable for each clock. Thus the number of variables used in REDis always linear to the number of clocks declared in the input system description. Experiment has been carried out to compare REDwith previous technologies. © Springer-Verlag Berlin Heidelberg 2000.