Naslov
Protocol Verification by the analysis of Reacheability Tree

Autori
Žagar, Drago

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), stručni

Izvornik
Wissenschaft fur die Praxis / - Pečuh, 1996

Skup
Wissenschaft fur die Praxis

Mjesto i datum
Pečuh, Mađarska, 06.1996

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Domaća recenzija

Ključne riječi
reachability tree; state perturbation technique; protocol; finite state machines

Sažetak
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.

Izvorni jezik
Engleski

POVEZANOST RADA