Dynamic model checking for concurrent programs in control system

Hao Liang¹, Yunfeng Ai², Huairong Shen³, Yongchao Zhao⁴

COMPUTER MODELLING & NEW TECHNOLOGIES 2014 18(12A) 275-281

¹Company of Postgraduate Management, the Academy of Equipment, Beijing 101416, China

²College of Engineering & Information Technology, University of Chinese Academy of Sciences, Beijing 100049, China

³Department ofspaceequipment, the Academy of Equipment, Beijing 101416, China

⁴National 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.