State space-based methods for validating model transformations in model checkers

Abstract Formal methods, including model checking, are rapidly gaining importance, especially in safety-critical domains like aerospace and automotive. Consequently, the systems to be verified are growing more complex and are described in diverse design languages, often expressive and ambiguous. However, model checkers operate on a formal representation of the model, which necessitates automated transformations from design models to formal representations. Misinterpretation of the input models’ semantics in this transformation can substantially alter behaviour, potentially compromising the validity of verification results. Complete formal verification of the transformation is impractical due to the informal semantics of the design languages, while other conventional software verification techniques (e.g. testing, review) often leave corner cases of semantics untested. This paper proposes an automated trace generation method for model checking tools that can be utilised in an end-to-end validation approach for model transformations to increase trust in verification results. Our contributions are as follows: (1) we adapt generic fault models to model transformations within model checkers; (2) we propose a state space-based trace generation technique on abstract reachability graphs; (3) we recommend how trace generation can be used in an end-to-end validation approach; and (4) we evaluate our work on the toolchain composed of the statechart modelling and verification framework Gamma and the abstraction-based model checker Theta . The experiment showed that state space-based techniques can generate a concise, but representative trace set showcasing the semantics encoded in the model transformation, unveiling subtle, previously undetected issues. Finally, we show the generalisability of the approach using demonstrations on SysML v2 and C code verification toolchains.