Safety Verification of Fault-Tolerant Distributed Components

Organisation:	INRIA Sophia Antipolis - Meditérranée / I3S lab and Institut Télécom - Télécom ParisTech (FRANCE) University Babes-Bolyai, Cluj-Napoca (ROMANIA)
Method:	FIACRE EXP SVL
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Component-based Systems.
Period:	2011
Size:	2900 lines FIACRE (43 processes) 330 lines EXP synchronization vectors 10 billion states
Description:	Proving a certain level of fault-tolerance in a distributed system is a very important task. In many application domains there cannot be any guarantees of the behavior of participating peers, for instance in P2P networks. Therefore, byzantine failure models, i.e., a completely non-deterministic behaviour must be assumed to be possible. It is very difficult to verify systems with such non-deterministic behavior, as the state space can increase dramatically. This work shows how the correctness of a distributed component based system can be verified even under the presence of byzantine failures. Assuming a maximal number of tolerable failures, it is shown that the approach based on counting the agreed truth values is correct. For this purpose, a hierarchical system model was built in the FIACRE language involving asynchronous communication implemented using message queues. The formal model was constructed and verified using CADP, in particular the EXP format for synchronization vectors, SVL for verification scripts, DISTRIBUTOR for distributed state space generation, and finally EVALUATOR 4.0 for verifying temporal logic properties.
Conclusions:	Using state-of-the-art modelling and verification techniques, this study shows the feasibility of verifying the correctness of fault tolerance in presence of byzantine failures. The efficient distributed state space creation and verification of CADP enabled a fully automatic correctness proof of the fault-tolerant system.
Publications:	[AmeurBoulifa-Halalai-Henrio-Madelaine-11] Rabea Ameur-Boulifa, Raluca Halalai, Ludovic Henrio, and Eric Madelaine. "Verifying Safety of Fault-Tolerant Distributed Components". Proceedings of the 8th International Symposium on Formal Aspects of Component Software FACS'11 (Oslo, Norway), LNCS vol. 7253, pages 278-295, Springer Verlag, 2011. Extended version available as Inria Research Report RR-7717, 2011. Available on-line from: http://hal.inria.fr/inria-00621264/en or from the CADP Web site in PDF or PostScript
Contact:	Eric Madelaine Inria Sophia-Antipolis - Meditérranée 2004, route des Lucioles B.P. 93 F-06902 Sophia Antipolis FRANCE Tel: +33 (0)4 92 38 78 07 Fax: +33 (0)4 92 38 76 44 Email: Eric.Madelaine@sophia.inria.fr
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