Research On Axiomatic Program Detection Method Based On Event Structure And Symbolic Computation

With the rapid development of computer technology,software applications have become more complex,so how to ensure the correct operation of programs has become the primary goal of software design.Especially in industries with high security requirements,how to analyze and detect applications has become a focus of software research.Traditional software testing methods rely on the experienced judgment of testers and extensive program testing.The formal method can transform the program code into mathematical logic.By analyzing the mathematical logic formula corresponding to the target program,it can verify whether the program meets the predetermined performance indicators,thus verifying the function and performance of the program.This article is based on the relevant theories of formal methods and applies knowledge of event structure and symbolic computation to study how to optimize the process structure of a program and verify its correctness.The main research contributions of this article are as follows:(1)This article proposes a modeling and analysis method for programs based on the relevant theory of event structure.By introducing the relevant theory of event structure,this article constructs the program model,converts the program statements into mathematical logic,and provides the corresponding syntax and semantics for the event structure model of the program.At the same time,by searching for action sequences in the event structure,the relationship formulas between different events were obtained,and a method for rewriting the process structure in the program was proposed.(2)This article proposes two reduction methods for process structures based on the theory of automorphism groups.The article analyzes the automorphism properties contained in process structures using the theory of automorphism groups,studies the automorphism properties between processes,proves the automorphism properties between different levels,and proposes a hierarchical process structure reduction method.Then this article takes the elementary event in the process structure as the starting point,analyzes and compares the isomorphism between the basic constituent elements,demonstrates the automorphism of the basic constituent elements,and proposes a process reduction method based on the Elementary event elements.Finally,the two process reduction methods mentioned above were combined and the characteristics of different reduction methods were compared through experimental analysis.(3)This article proposes an axiomatic method for verifying the correctness of programs based on the relevant theory of symbolic computation.This article first proposes a method for constructing logical polynomial equations corresponding to programming language by using formal methods to rewrite program statements.Then,theoretical research and analysis were conducted on how to use knowledge related to symbolic computation to solve program logic equations,and the correctness detection principle of the program was verified through propositions and proofs based on the relevant properties of characteristic set.Then this article demonstrates how to calculate the characteristic set of program logic equations by examples,and transforms the solving process of formal verification into calculating the remainder of the characteristic set and program assertions of polynomials,thereby achieving the purpose of formal verification of the program.