H-RAFT - heuristic reachability analysis for fault tolerance protocols modelled in SDL

Design flaws of fault tolerance techniques may lead to undesired consequences in particular fault cases under very special operating conditions. Such rare "fault tolerance holes" may be very difficult to reveal. This paper presents a novel approach directing the analysis towards potential weaknesses in a fault tolerance technique. A new algorithm based on special heuristics performs partial reachability analysis of SDL models describing fault-tolerant communication. It aims at finding violations of fault tolerance properties in an efficient way. The approach does not require knowledge of the model under investigation. The new algorithm is evaluated by experiments with realistic protocols - including a large model of an industrial system - and compared to the performance of known solutions.