Database of Case Studies Achieved Using CADP

Compositional Model Checking of Liveness Properties

Organisation: Eindhoven University of Technology (THE NETHERLANDS)

Method: networks of LTSs

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Distributed Systems.

Period: 2017

Size: up to 944,322,648 transitions.

Description: 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.

Conclusions: 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.

Publications: [DePutter-Wijs-17] 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
Contact:
Anton Wijs
Technische Universiteit Eindhoven
MetaForum 6.077
Postbus 513
5600 MB Eindhoven
The Netherlands
Tel: +31 (0)40 247 3991
Email: A.J.Wijs@tue.nl



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Mon Jan 14 17:03:23 2019.


Back to the CADP case studies page