Protocol Verification by the analysis of Reacheability Tree (CROSBI ID 485371)
Prilog sa skupa u zborniku | stručni rad | domaća recenzija
Podaci o odgovornosti
Žagar, Drago
engleski
Protocol Verification by the analysis of Reacheability Tree
In this paper the analyse of reachability tree for protocol errors exploration is presented. The state perturbation technique is based on the reachability analysis. The communicating processes are modeled as finite state machines. The base for the automatic protocol verification are formal methods. The protocols specification can be rigorously analyzed for completeness and consistency. By the protocol verificator "PERTURB" the given system state is systematically perturbed to find out all possible states, so that the new states become states for further perturbation. The states produced in that way are systematically examined if they contain errors, until all reachable states are passed. The perturbation technique applied in this paper successfully detects deadlock states, ambiguities, unspecified receptions, non executable interactions and channel overflows. Finally, on test protocol all kinds of errors are generated and then successfully detected.
reachability tree; state perturbation technique; protocol; finite state machines
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
1996.
objavljeno
Podaci o matičnoj publikaciji
Wissenschaft fur die Praxis
Pečuh:
Podaci o skupu
Wissenschaft fur die Praxis
predavanje
01.01.1996-01.01.1996
Pečuh, Mađarska