gLTSdiff: a generalized framework for structural comparison of software behavior

Structural comparison of state machine models – such as labeled transition systems and (extended) finite automata – is used for numerous applications, such as finding potential behavioral regressions in new oftware versions, evaluating the accuracy of different model learning algorithms, and fingerprinting software for security applications. The state-of-the-art LTSDiff structural comparison algorithm has limited assumptions, making it broadly applicable. However, representation-specific information is not taken into account, requiring adaptations to prevent sub-optimal or even invalid results. We introduce gLTSdiff, which generalizes and extends LTSDiff, allowing a wide range of state machine models to be compared, by recursively comparing over the structure of state and transition labels. Additional challenges that we faced while applying LTSDiff in industrial practice are also addressed by gLTSdiff, as it rewrites undesired difference patterns, supports comparison of any number of input models, and allows for an effort/quality trade-off.We formally define gLTSdiff, and make it available as an extensible open source library for structural model comparison. Using multiple large-scale industrial and open source case studies, we evaluate both its practical value and its various improvements.
This paper is an extended version of a MODELS 2023 conference paper [1], with as most prominent changes: extended background about LTSDiff; extended explanations and added examples for the introduced framework; extended discussion about combiners, including theorems and machine-checked proofs; improved structure, additional information, and added discussions of threats to validity, for the evaluations; and a newly-added related work section. This research was carried out as part of the Transposition project under the responsibility of TNO-ESI in co-operation with ASML. The research activities were supported by the Netherlands Ministry of Economic Affairs and Climate Policy, and TKI-HTSM.