Research On Theory And Application Of Multi-matching Nested Relation

The model is an indispensable bridge to connect between practical problems and scientific theories.In the real world,data with both a linear ordering and a hierarchically nested matching of items can be represented by one-to-one matching nested structure,such as parenthesis matching languages as well as the open and close tags in XML documents.Some relevant models are proposed for this structure,for instance Parenthesis Grammar,Bracketed Grammar,Balanced Grammar,Traceable automata,Nested Word Automata,etc.However,there exist some real-world problems which are beyond one-to-one matching.For instance,an n-to-one encryption and authentication scheme is used in group-oriented cryptography,which solves a practical problem that the number of the receivers is very small compared with the number of the senders and a receiver may serve millions of senders.Moreover,multiple threads can simultaneously read the same file,and one block of memory can be referenced by multiple pointers in programs,where there are multi-matching nested structures including one-to-n or n-to-one matching.However,the existing models are limited to one-to-one matching structures.With this motivation,this paper focuses on the theory relevant to multi-matching nested relations.The main work is summarized as follows:First of all,we propose a series of theories of multi-matching nested relation including the model of Multi-matching Nested Relation(MNR),Multi-matching Nested Word(MNW)and Multi-matching Nested Expression(MNE).Multi-matching nested relation consists of a sequence of linearly ordered positions,call,return,and internal,augmented with oneto-n or n-to-one matching nested edges from calls to returns(one-to-one matching should be a special case).After word encoding for multi-matching nested relations by introducing tagged letters,MNWs are obtained over a tagged alphabet for describing data with a multi-matching structure which has both a linear ordering and a hierarchically nested multimatching(one-to-one,one-to-n and n-to-one)of items.The sets of MNWs constitute Multimatching Nested Languages(MNL).Moreover,MNEs are introduced to formally define MNLs.Secondly,Multi-matching Nested Traceable Automata(MNTA)are proposed to express multi-matching nested languages.In an MNTA,states and input symbols are recorded for subsequent transitions.Specifically,a state is used to preserve part of the running history in order to determine the succeeding state,while the symbol is used to make comparison with the input one and indicate the one-to-n or n-to-one matching nested relation.The nondeterministic MNTA is proved to be as expressive as the deterministic one.In addition,we also explain the correspondence between MNTA and multi-matching nested relations.Besides,Multi-matching Nested Grammar(MNG)is also proposed to describe multi-matching nested languages.Further,the expressiveness of MNTA is proved to be the same as MNE and MNG.Finally,to show the practical application of the theory of multi-matching nested relation,a method based on MNTA is proposed for detecting memory defeats of C programs.Generally,memory is dynamically allocated in a program and freed after finishing used.An allocation is corresponding to a specific free,forming a one-to-one matching nested relation.Besides,memory is manipulated by pointers.If the manipulation is incorrect,the memory may be freed twice in a program execution path.An allocation and double frees constitute a one-to-n matching nested relation.In addition,memory can be read or written via pointers for many times.The relation between multiple usages and the final free is an n-to-one matching nested relation.Hence,there are three common memory defeats:(i)an allocated memory without free,(ii)double frees in a program execution path,(iii)the usage of a freed memory without being reallocated.The details of memory defeat detection are shown as follows.For a C program,a Control Flow Automaton(CFA)representation is built first.By unrolling a CFA,an Abstract Reachability Tree(ART)can be generated which shows the reachable state space of a program.Then a MNTA is constructed for describing memory defeats,where the transitions are constructed according to different types of edges in ART considering memory manipulations.Accordingly,to detect different memory defects of a program,it is determined whether there exists an unaccepted run.We have implemented the approach upon the software verification tool CPAChecker and evaluate it on two test suites.The experimental results figure out that the proposed approach is effective and feasible.