NRS approach to semantics of specification and testing of distributed systems.
|Title:||NRS approach to semantics of specification and testing of distributed systems.|
|Abstract:||In this thesis, we study a new semantic technique called NRS approach for modeling the behaviors of nondeterministic processes in distributed systems. The basic principle of this approach takes into account the abilities of each of the process and its environment to control execution behaviors of the whole system. System behaviors are therefore seen as the result of mutual influences of the process control and its environment control. The original idea comes from our experience in analyzing specifications for test generation and observing behaviors of processes under test, particularly telecommunications systems. The main objective of capturing this idea in formal semantics is to try to improve the applicability of formal semantics to the practical development of distributed systems. First, based on labelled transition systems, the process and environment controls are formalized as two formal objects: the nondeterministic rippling effect inside the process and the choice pattern enforced by the environment. By considering the mutual influences of these two objects, a semantic object denoted nondeterministic ripple set (NRS), is defined. Then, by means of synchronization trees, NRS is applied to a subset of CCS. As a semantic object, NRS can be used to describe various properties of processes. Next, based on NRS, we study a new equivalence between processes called nondeterministic ripple equivalence. Two processes are nondeterministic-ripple equivalent if they have the same set of nondeterministic ripple sets. An axiom system is provided for this equivalence, and its soundness and completeness are proved. Two auxiliary operators are introduced to model both process control and environment control algebraically. The algebraic representation of NRS is derived. This work provides a calculus for reasoning about process properties based on NRS. We then develop an application of NRS to process testing by formalizing a theory of testing. Distinct from other testing theories, we define tests based on the process under test such that each test can be related to a test purpose by means of the environment control. A testing preorder/equivalence called nondeterministic ripple acceptance testing is defined. It is proved that this testing preorder/equivalence possesses the same distinguishing power between processes as failure equivalence. Comparison of the NRS approach with other major semantic theories is discussed. It appears that NRS semantic interpretation is intuitively simple and practical for interpreting process behaviours in a distributed system. As for the distinguishing power of the nondeterministic ripple equivalence, it is proved that nondeterministic ripple equivalence is different from bisimulation equivalence, ready trace equivalence, refusal testing equivalence and readiness equivalence. Nondeterministic ripple equivalence is also proved to be different from failure equivalence, but we conjecture it implies failure equivalence. Extension of the NRS approach to recursive processes with internal actions is also briefly outlined. Finally, the contributions and practical applications of the NRS approach, in particular to conformance testing, are discussed. The application of the NRS semantic approach to conformance testing appears promising. This brings us back to our original inspiration from testing for NRS semantics, and lends support to the further development of a pragmatic formal semantics for testing processes in distributed systems.|
|Collection||Thèses, 1910 - 2010 // Theses, 1910 - 2010|