Options
Bounded DBM-based clock state construction for timed automata in Uppaal
Citation Link: https://doi.org/10.15480/882.4821
Publikationstyp
Journal Article
Date Issued
2023-02
Sprache
English
Author(s)
Lehmann, Sascha
Institut
TORE-DOI
Volume
25
Issue
1
Start Page
19
End Page
47
Citation
International journal on software tools for technology transfer 25 (1): 19-47 (2023-02)
Publisher DOI
Scopus ID
Publisher
Springer
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.
DDC Class
600: Technik
620: Ingenieurwissenschaften
Publication version
publishedVersion
Loading...
Name
s10009-022-00667-x.pdf
Size
2.91 MB
Format
Adobe PDF