A method and a tool for errors recovering in communication protocols

Communication protocols are very complex systems devoted to ensure error-free exchanges of informations between communicating entities. From their specification to their implementation, the different steps of protocols development still represent a hard work for designers. In this paper, we develop a method to help protocols designers in specification steps, such that the considered protocols are error-free and correspond as possible to the expected service. After their detection, it allows the suppression of errors such as unspecified receptions, deadlocks and blocking loops. The communicating entities are modelised by finite state machine (FSM) and the validation step is based on the construction of the reachability graph. After a correction oriented analysis of this graph, our method proposes sets of transitions of one or another FSM. The suppression of transitions in any of these sets eliminates the considered error without generating other errors. We finally present an application of our method to correct errors in a data transfer protocol