Program Static Analysis on Runtime Error for Aerospace Embedded Software

A novel program analysis method for run-time error detection based on property model is proposed. A property that describes the generation process of a certain run-time error is primarily given. And then, a finite state machine (FSM) is constructed to model the property. Finally, the branches for which the property-related behavior differs along the arms of the branch are abstracted, and the run-time error is found by analyzing these paths with path-sensitive and context-sensitive method. Experimental results show the proposed approach produces a better balance between the precision and efficiency compared with the latest run-time error detection methods.