Difference Bound Matrices (DBMs) are efficient data structures to represent clock constraints in timed automata. They are used in UPPAAL as the core data structure to represent time. This library features all the common operations such as up (delay, or future), down (past), general updates, different extrapolation functions, etc. on DBMs and federations. The library also supports subtractions and methods to merge DBMs.
Ruby-UDBM is a Ruby binding for the UPPAAL DBM library. It offers access to the federation type (set of DBMs) and most of its operations. In addition, a graphical viewer is provided to allow users to visualize updates on the fly. The library gives access to systems of constraints where clock constraints can be declared and used as intuitive formulas. This binding is intended to be a research prototyping tool as well as a teaching tool for students learning timed automata.
BDDs [bry86] (or more precisely ROBDDs) are efficient data structures for representing a boolean formula. They are widely used in formal verification, in particular symbolic model-checking. Ruby- BDD, based on Buddy, provides access to BDDs from Ruby, a powerful and very easy to use object-oriented language. The purposes are quick prototyping and education.
UPPAAL TIGA is an extension of UPPAAL, and implements the first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties. The tool provides a user-friendly graphical interface with its corresponding server, and a command line verifier.