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 the CADP Web 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

Back to the CADP case studies page