Research on model checking based on nested trees
Jin Guo · Journal of Hefei University of Technology · 2015
To solve the problems of structure abstract representation in the software verification process,taking into account the program sequence structure and the relationship between call and return,the definition of nested trees and nested state machine is given.Based on the data structure andμ-calculus,theμ-calculus of nested trees(NT-μ)is defined.The formula syntax of NT-μis based on the summary,and the model checking of summary class is presented.For the reason that the nodes in the nested state machine are finite,and the finite summary class in the nested state machine corresponds to the infinite summary in the nested tree,the method can improve the detection efficiency.