Patent Document ID: 7503060
Application ID: 10521671
Patent Flag: 1

Claim One:
1. A safety verification device of an electronic reactive system which is a cipher communication system or control system for a nuclear reactor or aircraft, represented by a set of function symbols, a set of rewriting rules, a set of axioms, a set of first terms, and a set of second terms to be verified, said set of axioms being a set consisting only a commutative law and an associative law, and said safety verification device of a reactive system comprising a processing unit, a recording unit, a translation unit, a simulation unit and a set operation unit, wherein: said set of function symbols, said set of rewriting rules, said set of axioms, said set of first terms, and said set of second terms to be verified are recorded in said recording unit; said translation unit is controlled by said processing unit to read out said set of axioms and said set of first terms from said recording unit and to generate, under said set of axioms, a first equational tree automaton which accepts said set of first terms; said simulation unit is controlled by said processing unit to read out said set of rewriting rules, said set of axioms and said set of first terms from said recording unit and to generate, under said set of rewriting rules and said set of axioms and using said first equational tree automaton as initial data, a second equational tree automaton which accepts said set of first terms and a set that comprises terms derived from said set of first terms; said set operation unit is controlled by said processing unit to generate, using said second equational tree automaton and said set of second terms to be verified, a fourth equational tree automaton by associating said second equational tree automaton with a third equational tree automaton which accepts said set of second terms to be verified and to determine whether or not a set accepted by the fourth equational tree automaton is an empty set; said second equational tree automaton is generated through first and second repetition processes; wherein said first repetition process comprises: (A) setting said first equational tree automaton to initial data; (B) selecting an element p from a first group which consists of position information in a tree-structure when left sides of equations, each of said equations corresponding to a rewriting rule in said set of rewriting rules, are described in tree-structure, wherein said element p is positioned at the end of said tree-structure; (C) determining a set of third terms by rewriting all terms which are included in a fifth equational tree automaton obtained in a last process performed according to the rewriting rule ƒ(c p.l tl ,. .. , c p.n tn )-->c p l|p , wherein a function symbol of said element p is described as ƒ, argument terms are described as t l ,. .. , t n , and a term l|p corresponding to said element p is described as ƒ(t l ,. .. , t n ); (D) obtaining a sixth equational tree automaton by performing repeatedly said (B) selecting and (C) determining processes regarding all elements p positioned at the ends of said tree-structure of said first group; and wherein said second repetition process comprises: (E) setting said sixth equational tree automaton to initial data; (F) selecting an element q from a second group which consists of position information in a tree-structure when right sides of equations, each of said equations corresponding to a rewriting rule in said set of rewriting rules, are described in tree-structure, wherein said element q is positioned at the end of said tree-structure; (G) determining a set of fourth terms by rewriting all terms which are included in a seventh equational tree automaton obtained in a last process performed according to the rewriting rule ƒ(d q.l tl ,. .. , d q.n tn )-->d q r|q , wherein a function symbol of said element q is described as ƒ, argument terms are described t l ,. .. , t n , and a term r|q corresponding to said element q is described as ƒ(t l. .. , t n ); and (H) obtaining said second equational tree automaton by performing repeatedly said (F) selecting and (G) determining processes regarding all elements q positioned at the ends of said tree-structure of said second group.