INRIA Sophia Antipolis - Meditérranée / I3S lab and
Institut TÚlÚcom - TÚlÚcom ParisTech (FRANCE)
University Babes-Bolyai, Cluj-Napoca (ROMANIA)
CADP (Construction and Analysis of Distributed Processes)
2900 lines FIACRE (43 processes)
330 lines EXP synchronization vectors
10 billion states
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.
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.
Rabea Ameur-Boulifa, Raluca Halalai, Ludovic Henrio, and
"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
Inria Sophia-Antipolis - Meditérranée
2004, route des Lucioles
F-06902 Sophia Antipolis
Tel: +33 (0)4 92 38 78 07
Fax: +33 (0)4 92 38 76 44
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|