Research On The Reasoning Methods Of Errors Polynomial

With the application and development of formal verification technology,theorem proving and model checking have complementary advantages,and play an increasingly important role in the verification of safety-critical systems(aviation industry,lunar exploration project,autonomous driving technology,etc.).Theorem proving technology needs strict mathematical deduction to prove whether the system satisfies the specific security properties,and some verification tools based on theorem proving have appeared.Nevertheless,errors are common to systems.At present,most verification theories based on theorem proving seldom consider the error parameters within systems.Hence,it is of great theoretical and practical significance to apply formal verification technology to the safety-critical systems with errors.On the other hand,polynomial algebra system has a strong ability to describe continuous data exchange and continuous state,and in recent years,polynomial algebra(a branch of symbolic computation)has also made great progress.For instance,real root isolation algorithm,Gr(?)bner basis,Wu’s method,research of solution of semi-algebraic system.Based on the above thinking and researching in this field for several years,we have made innovations in the following aspects.(1)For reasoning method of errors linear assertion: it is proved that the zero set of error linear assertion is a convex set,and a method for finding all vertexes of errors linear assertion is proposed,and the correctness of this method is proved.By analyzing related concepts and theorems,the problem to judge whether there is implication relationship between linear error assertions is converted to the problem to judge whether the vertexes of the precursor assertion are contained in the zero set of the successor assertion.Finally,the method’s applications to uniform and accelerated motion of train are given,and a large number of random errors parameters are used to simulate and test this method.(2)For reasoning method of non-linear errors polynomial assertion: the implication relationship between errors polynomial assertion can be converted to inclusion relationship between zero sets of errors polynomial assertions;the errors polynomial assertion can be then transformed into first-order semi-polynomial logic.Combined with the quantifier elimination method based on cylindrical algebraic decomposition,the judgment on the inclusion relationship between zero sets of errors polynomial assertions is converted to the quantifier elimination problem on a specific first-order semi-polynomial logic.Finally,an example of target interception is given,and the correctness of our method is also verified by large-scale random errors parameters.(3)Reasoning method of errors polynomial assertion combined with errors probability information: Using truncated normal interval to describe the error,and partially simplifying the operations of truncated normal intervals.A reasoning method combined with the probability information of error is proposed.According to the statistical information of errors,our method can judge the potential non-error faults of the system earlier.Finally,the application of this method to the two-body problem of train acceleration power distribution is given.Through the test with large-scale random errors parameters,the simulation results are consistent with the theoretical reasoning results.(4)In error semantics,interval and truncated normal interval are used to describe errors.Two problems existing on interval operations(irreversibility and range expansion)are analyzed.Our reasoning methods(error linear assertion and nonlinear error polynomial reasoning method,reasoning method combined with error probability information)greatly avoid the two problems.because,when the upper bound and lower bound of interval numbers are equal,error polynomial assertion degenerates into classical polynomial assertion.Hence errors polynomial assertion is logically consistent with the classical polynomial assertion.The zero sets of errors polynomial assertions are also self-consistent with the zero sets of classical polynomials.The equivalent condition on the implication relation of errors polynomial assertions is also given.