Automata Specification Mining Based On Data Classifier Inference Algorithm

The ability to reverse engineer software behavior specifications is very useful for extensive software maintenance and verification.Current reverse engineering technologies focus on controlling specific behaviors(e.g.,in the form of finite state machines)or data-specific behaviors(e.g.,as pre/post conditions or invariants).However,the typical software behavior is usually the product of the two,and the specification must combine the two aspects to fully represent the operation of the software.The extended finite state machine provides such a specification.To capture the behavior specifications of software systems more comprehensively,this thesis designs and implements an extended finite state machine specification mining tool,which takes an improved extended finite state machine specification mining algorithm as the core to mine extended finite state machine from the execution trace.This specification mining method is mainly divided into four stages:generation of prefix tree,selection of state merge,verification of time sequence rules,and state merge.When generating a prefix tree acceptor,this tool marks the transition by function name and data variable value(input parameter)corresponding to each function and uses the inferred data relationship and running traces to generate the prefix tree acceptor.When selecting state merging,this tool uses an evidence-driven state merging algorithm as the basis of state merging.When judging whether two states are equivalent or not,besides judging whether the labels(function name)on the transformation are the same or not,it also uses data relations as conditional constraints to select possible equivalent state pairs.When verifying temporal rules,to solve the problem that the merge violating the temporal properties may introduce inaccurate generalization after the possible equivalent state pairs are obtained,the temporal rules are added to verify whether the two equivalent state pairs can be merged.The original temporal rule inferring technique can only infer future temporal rules,the temporal inferring tool FPTRules developed in this thesis not only can infer future temporal rules but also can infer past temporal rules,with the two rules to verify can keep automaton temporal properties,avoid the relationship between the nonlocal damage,to solve the problem that the standard overgeneralization.When merging state,this tool is different from the general state merging algorithm.In addition to the label need to be merged,the data variable values corresponding to the above transformation also need to be merged.After state merging,the consistent test should be carried out to ensure that the incoming transition of the merged state and the predicted value of the data variable are consistent with the next outgoing transition of the state.Based on the improved extended finite machine specification mining tool developed in the above stage,this thesis can effectively mine the extended finite state machine.Through experimental evaluation,the improved extended finite machine specification mining specification algorithm proposed in this thesis can improve the accuracy of extended finite machine.In a word,the improved extended finite machine specification mining tool developed in this thesis can mine a finite state machine which can comprehensively represent the behavior of software system.