Temporal dynamic push-down network converting method

Abstract

The invention discloses a temporal dynamic push-down network converting method used for describing real-time concurrent recursive modeling including recursive and dynamic thread creation. The converting method includes the steps that a global clock for describing continuous time and real number clocks capable of describing global variables and stack character ages related to time are introduced in DPN, so that asynchronous communication is achieved based on shared memories, and a real-time concurrent system with dynamic thread creation is modeled; for a clock equivalence technology based on integer division, an optimization technology based on a clock key point is given, a clock interval is reduced, and therefore state space obtained after conversion is reduced. As temporal dynamic push-down networks are abstract models of one kind of real-time concurrent recursive programs, the models are converted into the dynamic push-down networks by the clock equivalence optimization technology based on the key point, in this way, it is detected that the models are errors or bugs in the corresponding concurrent recursive program by verifying whether execution of the dynamic push-down networks operates into an error state or not.

Description

technical field [0001] The invention belongs to the field of software security and reliability research, relates to a verification method for a multi-threaded concurrent recursive program, is a reachability solution technology applicable to an abstract model of a multi-threaded concurrent recursive program containing time, and specifically relates to a time dynamic The transformation method for the pushdown network. Background technique [0002] With the development of multi-core technology, concurrent programs have become a hot spot in current program design research. Due to the uncertainty of concurrent execution, it is difficult for traditional testing methods to find hidden errors and loopholes in programs. Model checking is an automatic verification technology through exhaustive search, which has become an important means to ensure the safety and reliability of programs, and can be used as a supplement to testing methods. Reachability analysis is an important core tec...

AI Technical Summary

Problems solved by technology

[0004] Since the above model cannot describe the interaction between threads in a real-time multi-threaded concurrent recursive system, for real-time multi-threaded concurrent recursive programs, the formal verification of such programs will cause the problem of state space explosion, which brings great difficulties to the verification

Images