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
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Fontana, Peter; Cleaveland, Rance: A menagerie of timed automata (2014)
- Fontana, Peter; Cleaveland, Rance: The power of proofs: new algorithms for timed automata model checking (2014)
- Herbreteau, Frédéric; Srivathsan, B.: Coarse abstractions make Zeno behaviours difficult to detect (2013)
- Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen: A survey of timed automata for the development of real-time systems (2013)
- Herbreteau, Frédéric; Srivathsan, B.: Coarse abstractions make Zeno behaviours difficult to detect (2011)