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 statespaces. 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 fixpoint evaluation, and coverage analysis of dense-time statespaces. 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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element