Data flow anomaly analysis based on model checking
Jun Niu · Computer Engineering and Applications Journal · 2011
The execution of program embodies flows of data in variable.A novel method is proposed to detect data flow anomaly including variable undefined or defined but not referenced or multi-used.The trust pattern of program is defined and program is translated into finite state machine.Based on ALCCTL temporal logic and model checking,verification model satisfies the trust pattern defined.Experiment shows that this method is effective and has been implemented in a defect-oriented testing system.