Runtime Monitoring with Union-Find Structures

TitleRuntime Monitoring with Union-Find Structures
Publication TypeConference Paper
Year of Publication2016
AuthorsDecker, N, Harder, J, Scheffel, T, Schmitz, M, Thoma, D
Conference NameTools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016
VolumeLNCS,
PublisherSpringer
AbstractThis paper is concerned with runtime verification of object-oriented software system. We propose a novel algorithm for monitoring the individual behaviour and interaction of an unbounded number of runtime objects. This allows for evaluating complex correctness properties that take runtime data in terms of object identities into account. In particular, the underlying formal model can express hierarchical interdependencies of individual objects. Currently, the most efficient monitoring approaches for such properties are based on lookup tables. In contrast, the proposed algorithm uses union-find data structures to manage individual instances and thereby accomplishes a significant performance improvement. The time complexity bounds of the very efficient operations on union-find structures transfer to our monitoring algorithm: the execution time of a single monitoring step is guaranteed logarithmic in the number of observed objects. The amortised time is bound by an inverse of Ackermann's function. We have implemented the algorithm in our monitoring tool Mufin. Benchmarks show that the targeted class of properties can be monitored extremely efficient and runtime overhead is reduced substantially compared to other tools.
Refereed DesignationRefereed
Bibtex: 
@inproceedings {1204,
	title = {Runtime Monitoring with Union-Find Structures},
	booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016},
	volume = {LNCS,},
	year = {2016},
	publisher = {Springer},
	organization = {Springer},
	abstract = {This paper is concerned with runtime verification of object-oriented software system. We propose a novel algorithm for monitoring the individual behaviour and interaction of an unbounded number of runtime objects. This allows for evaluating complex correctness properties that take runtime data in terms of object identities into account. In particular, the underlying formal model can express hierarchical interdependencies of individual objects. Currently, the most efficient monitoring approaches for such properties are based on lookup tables. In contrast, the proposed algorithm uses union-find data structures to manage individual instances and thereby accomplishes a significant performance improvement. The time complexity bounds of the very efficient operations on union-find structures transfer to our monitoring algorithm: the execution time of a single monitoring step is guaranteed logarithmic in the number of observed objects. The amortised time is bound by an inverse of Ackermann{\textquoteright}s function. We have implemented the algorithm in our monitoring tool Mufin. Benchmarks show that the targeted class of properties can be monitored extremely efficient and runtime overhead is reduced substantially compared to other tools.},
	author = {Normann Decker and Jannis Harder and Torben Scheffel and Malte Schmitz and Daniel Thoma}
}