42results about How to "Reduce the number of states" patented technology

The invention belongs to the field of computer application technology and discloses an interpolation-based model checking path reduction method and a computer. According to the method, a C program isread, syntactic and semantic analysis is performed on the C program, and a control flow graph (CFG) is extracted from an abstract syntax tree; a safety (S) interpolation value and an error (E) interpolation value are added to the CFG, and the CFG is expanded; and in the process of generating an ARG according to the CFG, whether the safety interpolation value and the error interpolation value are contained in a current path formula is judged in each state. Through the method, by calculating the S interpolation value and the E interpolation value, checking efficiency is improved, and a model checking algorithm can be better applied to a large-scale program; unnecessary exploration of the S interpolation value is avoided, and the number of states of the ARG is greatly reduced; the E interpolation value can be used for quickly judging whether a true counterexample path exists in the program, verification of the program is accelerated, and efficiency is improved; and useless nodes and edgesin the CFG are clipped, so that a traversal state space is reduced.

The invention discloses a rapid circulating expansion detection method and belongs to the technical field of software model detection. The method comprises the following steps of: 1) limiting a value range of each variable in a testing space and initializing the state in the testing space into all states meeting preconditions of a tested program in the limited range of the tested program; 2) randomly selecting an undetected state s and calling the tested program, and recording an executing path p of the tested program, by which the state s passes, and dynamic executing information; 3) sequentially calculating and detecting a circulating expansion similar path p' of the executing path p according to the dynamic executing information and checking whether all the states represented by a path restricting condition of the path p' are right or not, if so, cutting off the states passing through the detection from the testing space, and if not, printing a wrong state and giving out a counter example; and 4) carrying out iteration detection on all the states in the testing space. The method disclosed by the invention reduces the quantity of executed testing examples and increases the detection speed.