Univ. Grenoble Alpes, LIG, and Inria Grenoble - Rhône-Alpes (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
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. Model-based verification methods, which work
on LTS (Labelled Transition System) models of distributed systems,
enable to automatically chase and find bugs that would be very
difficult, if not impossible, to detect manually. Equivalence checking
determines whether two LTSs (typically modelling the requirements and
the implementation) are equivalent modulo a bisimulation relation.
When the LTSs are not equivalent, the checker returns a Boolean verdict
accompanied by a counterexample, which is typically a sequence of
actions that, when executed in the two LTSs, leads to a couple of
non-equivalent states. 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 not
the same situation from a design or debugging point of view.
This work proposes a set of metrics for quantifying the similarity of two behavioural models described using LTSs. The approach starts by computing the classes of bisimilar and non-bisimilar states using partition refinement. Then, a set of global and local metrics for each couple of non-bisimilar states is computed, which enables to build a matrix with a measure between 0 (totally different states) and 1 (bisimilar states) for each couple of states. This is done by combining several criteria, such as the matching of incoming/outgoing transitions, the similarity of neighbour states, the shortest distance from the initial state, and the distance to the closest bisimilar state. Finally, a global measure of similarity of both LTSs is computed based on this matrix.
The computation of partition refinement, matrix, and similarity measures was implemented in the DLTS tool, which takes as inputs two LTSs in the textual AUT format (obtained by compiling LNT formal descriptions using the CADP compilers). DLTS was applied on about 200 LTSs, and its usage is illustrated on two case-studies in different areas: Internet of Things (conformance between a candidate composition of devices and a goal composition) and BPMN business process engineering (detection of similarities between a process and its evolved version).
Better understanding and measuring the difference between two
behavioural models can be of interest in many different contexts
and application areas. For instance, it can be used for debugging
purposes when the equivalence checking counterexample is not sufficient
for detecting the source of the bug, for measuring the distance between
two versions of a software, and for process model matching in the
context of business process management.
"Quantifying the Similarity of Non-bisimilar Labelled Transition
Systems". Science of Computer Programming 202, 2021.
Available on-line at: http://hal.inria.fr/hal-03017666/en
or from the CADP Web site in PDF or PostScript
Inria Grenoble - Rhône-Alpes
655, avenue de l'Europe
38330 Montbonnot Saint Martin
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|