REDLIB for the Formal Verification of Embedded Systems

To promote the technology of dense-time system model-checking in both academia and industry, we developed a library, called REDLIB, which supports full TCTL model- checking of dense-time automata with multiple fairness assumptions. REDLIB uses the BDD-like diagrams for the efficient representation and manipulation of dense-time state- spaces. Users can use the procedures in REDLIB to quickly construct dense-time models and carry out basic Boolean and state-space operations, postcondtion/precondition calculation, state-space representation normalizations, greatest fixpoint calculation, parametric safety analysis of linear hybrid systems, speed-up techniques for greatest fix- point evaluation, and coverage analysis of dense-time state- spaces. REDLIB also has a preprocessor that allows for high-level constructs like arrays, message channels, dynamic memory allocation, procedure calls, and timers. In this article, we discuss the features of REDLIB and give small examples to show how to use REDLIB.