UPPAAL DBM Library

DBMs [dill89, rokicki93, lpw:fct95, bengtsson02] are efficient data structures to represent clock constraints in timed automata [ad90]. They are used in UPPAAL [lpy97, by04, bdl04] as the core data structure to represent time. The 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. The API is in C and C++. The C++ part uses active clocks and hides (to some extent) memory management.

• Reliable
  The DBM library has an extensive test suite with an extra alternative implementation of the algorithms. This implementation has also been tested on countless case studies.
• Performant
  The DBM library is the fruit of many years of development of UPPAAL, bringing to the mainstream efficient algorithms to manipulate DBMs. The API is available in C and C++.
• Current
  The DBM library is based on the latest internal development version of UPPAAL, containing the latest performance and language improvements.

The general form of the constraints is the following: x_i - x_j <=> c_ij, where x_i and x_j are clocks (one of them can be "zero clock" which is always zero) and <= can be one of {<, <=, =, >=, >} and c_ij is an integer constant.

For more details please see wiki pages.

Build

The following packages need to be installed:

• bash
• cmake
• GCC, clang or other C++17 compiler.
• xxHash
• UUtils
• doctest (just for unit tests)

The dependencies can be installed locally into local directory by running getlibs.sh:

./getlibs.sh

Compile source with release optimizations:

cmake -B build-release -DCMAKE_BUILD_TYPE=Release -DCMAKE_PREFIX_PATH=$PWD/local
cmake --build build-release

Compile source with release optimizations and unit tests:

cmake -B build-release -DCMAKE_BUILD_TYPE=Release -DCMAKE_PREFIX_PATH=$PWD/local -DUDBM_WITH_TESTS=ON
cmake --build build-release
(cd build-release ; ctest)

Compile source with debug, sanitizers and unit tests:

cmake -B build-debug -DCMAKE_BUILD_TYPE=Debug -DCMAKE_PREFIX_PATH=$PWD/local -DUDBM_WITH_TESTS=ON -DSSP=ON -DUBSAN=ON -DASAN=ON
cmake --build build-debug
(cd build-debug ; ctest)

References

• [dill89] David L. Dill. Timing Assumptions and Verification of Finite-State Concurrent Systems. LNCS 407. Springer Berlin 1989, pp 197-212.
• [rokicki93] Tomas Gerhard Rokicki. Representing and Modeling Digital Circuits. Ph.D. thesis, Standford University 1993.
• [lpw:fct95] Kim G. Larsen, Paul Pettersson, and Wang Yi. Model-Checking for Real-Time Systems. Fundamentals of Computation Theory 1995, LNCS 965 pages 62-88.
• [bengtsson02] Johan Bengtsson. Clocks, DBM, and States in Timed Systems. Ph.D. thesis, Uppsala University 2002.
• [ad90] Rajeev Alur and David L. Dill. Automata for Modeling Real-Time Systems. International Colloquium on Algorithms, Languages, and Programming 1990, LNCS 443 pages 322-335.
• [lpy97] Kim G. Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a Nutshell. International Journal on Software Tools for Technology Transfer , October 1997, number 1-2 pages 134-152.
• [by04] Johan Bengtsson and Wang Yi. Timed Automata: Semantics, Algorithms and Tools. Concurrency and Petri Nets 2004, LNCS 3098.
• [bdl04] Gerd Behrmann, Alexandre David, and Kim G. Larsen. A Tutorial on UPPAAL. 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-RT'04), LNCS 3185.