Home

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.

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.