Publisher DOI: 10.1007/s10009-022-00667-x
Title: Bounded DBM-based clock state construction for timed automata in Uppaal
Language: English
Authors: Lehmann, Sascha 
Schupp, Sibylle 
Issue Date: 8-Sep-2022
Source: International journal on software tools for technology transfer 31 (in Press) : (2022)
Abstract (english): 
When the simulation of a system, or the verification of its model, needs to be resumed in an online context, we face the problem that a particular starting state needs to be reached or constructed, from which the process is then continued. For timed automata, especially the construction of a desired clock state, represented as a difference bound matrix (DBM), can be problematic, as only a limited set of DBM operations is available, which often does not include the ability to set DBM entries individually to the desired value. In online applications, we furthermore face strict timing requirements imposed on the generation process. In this paper, we present an approach to construct a target clock state in a model via sequences of DBM operations (as supported by the model checker Uppaal), for which we can guarantee bounded lengths, solving the present problem of ever-growing sequences over time. The approach forges new intermediate states and transitions based on an overapproximation of the target state, followed by a constraining phase, until the target state is reached. We prove that the construction sequence lengths are independent of the original trace lengths and are determined by the number of system clocks only, allowing for state construction in bounded time. Furthermore, we implement the (re-)construction routines and an extended Uppaal model simulator which provides the original operation sequences. Applying the approach to a test model suite as well as randomly generated DBM operation sequences, we empirically validate the theoretical result and the implementation.
ISSN: 1433-2779
Journal: International journal on software tools for technology transfer 
Institute: Softwaresysteme E-16 
Document Type: Article
Project: Projekt DEAL 
Appears in Collections:Publications without fulltext

Show full item record

Page view(s)

checked on Dec 1, 2022

Google ScholarTM


Add Files to Item

Note about this record

Cite this record


Items in TORE are protected by copyright, with all rights reserved, unless otherwise indicated.