Modeling And Verification Of Systems Based On Computational Models

The theory of computation is a foundation of computer software and theory. The development of it is directly affect the work the scientists do now. Turing Machines become the high forms of automaton and models of computation that possess the strongest simulated capability so far. But it is not convenient to describe systems with parallel,concurrency,asynchronous,distributional,randomness and higher level of abstraction. Petri Nets are computational models that presented to describe concurrency behaviors and crucial tools for formulation software and graphical representation, with advantage of intuitiveness, understandability and usability. The information of model structure and dynamic behavior can be given by verification and it can be used to promote system.Based on the meaning of automaton, this paper will reduce Petri nets into a high level form of the development of it. A detailed description and comparison about Turing machine,Petri net,extended Petri net with inhibitor arc and their simulated capability,analysis technique and respective advantage will be presented in this paper. Then, consider the simulated capability of Turing Machine, make use of the multitape computing model, the form of transition function. This paper establishes a method to Turing machine call and Turing machine recursive technology, meanwhile, give correlative proofs about Turing machine call and Turing machine recursive invocation are Turing recognizable; Consider the simulated capability of Petri net,extended Petri nets with inhibitor arc, a hierarchical model of online judge with B/S was constructed by P/T Nets. According to the function, we presented some results which were used so far for checking the correctness of system; a model of Data Exchange Nets(DEN) was constructed based on the extended Petri Nets with inhibitor arcs. The correctness of the model is being proved at the end of this paper.