Hrvatska znanstvena Sekcija img
3 gif
 About the project
4 gif
Basic search
Advanced search
Statistical data
Other bibliographies
Similar projects
 Catalogues and databases

Bibliographic record number: 91673


Authors: Žagar, Drago
Title: Protocol Verification by the analysis of Reacheability Tree
Source: Wissenschaft fur die PraxisPech, Hungary :
Meeting: Wissenschaft fur die Praxis
Location and date: Pečuh, Madžarska, June, 1996.
Keywords: reachability tree; state perturbation technique; protocol; finite state machines
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.
Type of meeting: Predavanje
Type of presentation in a journal: Full-text (1500 words and more)
Type of peer-review: Domestic peer-review
Original language: ENG
Category: Expert

  Print version   za tiskati