Equivalence checking is an established technique for automatically verifying that two behavioural models (Labelled Transition Systems, LTSs) are equivalent from the point of view of an external observer. When these models are not equivalent, the checker returns a Boolean result with a counterexample, which is a sequence of actions leading to a state where the equivalence relation is not satisfied. However, this counterexample does not give any indication of how far the two LTSs are one from another. One can wonder whether they are almost identical or totally different, which is quite different from a design or debugging point of view. In this paper, we present an approach for measuring the similarity between two LTS models. The set of metrics is computed automatically using a tool we implemented. Beyond presenting the foundations of the proposed solution, we will show how it can be applied to two concrete application domains for supporting the construction of IoT applications on the one hand and for contributing to the process model matching problem on the other.

۱٫ Introduction

Designing and developing distributed software has always been a tedious and error-prone task, and the ever increasing software complexity is making matters even worse. Although we are still far from proposing techniques and tools avoiding the existence of bugs in a software under development, we know how to automatically chase and find bugs that would be very difficult, if not impossible, to detect manually.

Model checking [1] is an established technique for automatically verifying that a model (Labelled Transition System, LTS), obtained from higher-level specification languages such as process algebra, satisfies a given temporal property. Equivalence checking [16] is an alternative solution to model checking and is very helpful to check that two models (requirements and implementation for instance) are equivalent from the point of view of an external observer. When these models are not equivalent, the checker returns a Boolean result with a counterexample, which is a sequence of actions leading to a state where the equivalence relation is not satisfied. However, this counterexample does not give any indication of how far the two LTSs are one from another. One can wonder whether they are almost identical or totally different, which is quite different from a design or debugging point of view