A unified approach for equivalence relations of indeterministic distributed systems (with application to network protocols).
|Title:||A unified approach for equivalence relations of indeterministic distributed systems (with application to network protocols).|
|Abstract:||Equivalence relations are criteria for comparing the behavior of systems. They have important applications in the verification and testing of communications protocols. This thesis presents our investigation on equivalence relations in two parts. Part One contains mainly the theoretical results. It first gives a survey on many important equivalence relations. It then proposes new types of reachability for indeterministic distributed systems and a unified definition which reveals the essential and common features of many equivalence relations. This uniform approach points out that the various equivalence relations differ from one another mainly in the domain of the action sequences, the types of reachability and the observable properties of the reached sets of states. Exhibited behavior equivalence relation is redefined and a new polynomial time algorithm for its verification is presented. Three reduction methods among the equivalence relations are discussed and a number of results on property-preserved transformations are given. A proof that EB equivalence is stronger than testing equivalence in non-strongly convergent labeled transition systems is presented. A disproof of the conclusion existing in literature that EB equivalence is stronger than weak equivalence is provided. Part Two reports our implementation of the various verification algorithms in a system call LTS-EVS in the Sun Workstation.|
|Collection||Thèses, 1910 - 2010 // Theses, 1910 - 2010|