Skip to main content.

Welcome!

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.

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.

Latest News

DBM library version 2.0.8 released

6 May 2011

A few bugs have been fixed and the library has support for 64-bit.

Python binding version 0.1 released

21 Mar 2011

A new binding for the DBM library has been released. We now support Python.

Ruby binding version 0.11 released

10 Aug 2010

This is a maintenance release compiled against the DBM library 2.0.7.

DBM library version 2.0.7 released

10 Aug 2010

This is a maintenance release. Some new functions have been added and a leak in partition has been fixed.

Ruby binding version 0.10 released

19 Sep 2007

The new functions of the DBM library have been made accessible from the binding and some more have been added. A relation cache has been added.

DBM library version 2.0.6 released

19 Sep 2007

This is a maintenance release. Some new functions have been added and a leak in resize has been fixed.

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.