Dynamic model checking for concurrent programs in control system
Hao Liang1, Yunfeng Ai2, Huairong Shen3, Yongchao Zhao4
COMPUTER MODELLING & NEW TECHNOLOGIES 2014 18(12A) 275-281
1Company of Postgraduate Management, the Academy of Equipment, Beijing 101416, China
2College of Engineering & Information Technology, University of Chinese Academy of Sciences, Beijing 100049, China
3Department ofspaceequipment, the Academy of Equipment, Beijing 101416, China
4National Defense University, Department of battle command and training, Beijing 100091, China
In recent years, the complexity of programs incontrol systems continues to increase with the growing of automation. Concurrent programming methods have been widely used in designing. However, it is a lack of effective concurrent error checking tool for control system programs. Therefore we proposed a statefull DPOR method with sleep set, and designed a dynamic checking tool for control systems Multithread programs, in which we expand Labelled Transition Systems to record the priority of interrupt and the enabled flag as a system model. We gave formal description for deadlock, data race and atomicity violation three concurrency errors. Finally we realize the testing tool which can detect multi-threaded and multi-interrupt concurrent errorsin the control system. The result of Experiment shows that our method has higher efficiency and accuracy.