Eindhoven University of Technology (THE NETHERLANDS)
networks of LTSs
CADP (Construction and Analysis of Distributed Processes)
up to 944,322,648 transitions.
Model checking is one of the most successful approaches for the
analysis and verification of the behaviour of concurrent systems.
However, a major issue is the so-called state space explosion problem:
the state space (or Labelled Transition System, LTS for short) of a
concurrent system tends to increase exponentially as the number of
parallel processes increases linearly. Compositional model checking
approaches attempt to limit state space explosion by iteratively
combining behaviour of some of the components in the system and
reducing the result modulo an appropriate equivalence relation.
This relation should be a congruence for parallel composition where
synchronisations between the components may be introduced. An
equivalence relation preserving both safety and liveness properties
is divergence-preserving branching bisimulation (DPBB).
In this work, it is proven that DPBB is a congruence for the parallel composition of synchronising LTSs. Also, a method is devised to safely decompose an LTS network in components such that the composition of the components is equivalent to the original LTS network. The effectiveness of compositionally constructing state spaces with intermediate DPBB reductions in comparison with the classical, non-compositional state space construction is demonstrated using CADP. Twelve models of concurrent systems have been considered for minimisation modulo DPBB, each model being minimised with respect to a given liveness property. The composition approach used is the smart reduction strategy implemented in CADP. The classical approach, where the full state space is constructed at once and no intermediate minimisations are applied, is the root reduction strategy of CADP. Root reduction performs best for relatively small models, whereas smart reduction starts performing better for moderately sized models, being several hours faster for large models.
The LTS network model implemented in CADP provides a useful framework
for experimenting compositional verification approaches.
The experiments conducted in this study show that compositional
reduction is most efficient when it is expected that components reduce
significantly and highly interleaving components are added last.
S. de Putter and A. Wijs.
Compositional Model Checking is Lively.
Proceedings of the 14th International Conference on Formal Aspects of
Component Software (FACS'17), Braga, Portugal, LNCS vol. 10487,
pages 117-136. Springer Verlag, October 2017.
Available on-line at: http://facs2017.di.uminho.pt/sites/default/files/De-PutterWijs-facs2017.pdf
and from our FTP site in PDF or PostScript
Technische Universiteit Eindhoven
5600 MB Eindhoven
Tel: +31 (0)40 247 3991
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|