The Design of Dynamic Checking Tool for VXWORKS Systems Concurrent Program

作者: 梁昊 :装备学院,研究生管理大队,北京; 艾云峰 :中国科学院大学,工程管理与信息技术学院,北京; 沈怀荣 :装备学院,航天装备系,北京; 赵永超 :国防大学,作战与指挥训练教研部,北京;

关键词: 实时嵌入式系统并发程序多重中断多线程并发错误Real-Time Embedded Systems Concurrent Program Multiple Interrupts Multithread Concurrency Errors



Abstract: In recent years, with the improving degree of automation of real-time embedded systems, their design complexity continues to increase. Concurrent programming methods were widely used in designing. But due to real-time embedded system interrupts and threads overlap, in the testing and checking process of real-time embedded system, there is always lack of an effective program testing tool. So we designed a testing tool for VXWORKS systems dynamic concurrent programs. We use Labeled Transition Systems as a system of concurrent programming model, and have given formal definition for common concurrency error, and use of partial order reduction algorithm to reduce the state space of the program. Finally, we have realized the testing tool which can detect multi-threaded and multi-interrupt program concurrent errors.

文章引用: 梁昊 , 艾云峰 , 沈怀荣 , 赵永超 (2014) VXWORKS系统并发程序动态测试工具设计。 软件工程与应用, 3, 86-96. doi: 10.12677/SEA.2014.33011


[1] 吴学光, 文艳军, 王戟, 傅秀涛, 綦艳霞, 顾斌 (2011) 多重中断C程序中数据竞争及原子性违背检测. 计算机科学与探索, 12, 1086-1093.

[2] Regehr, J. and Cooprider, N. (2007) Interrupt verification via thread verification. Electronic Notes in Theoretical Computer Science, 174, 139-150.

[3] Hofer, W., Lohmann, D., Scheler, F., Schroder-Preikschat, W. (2009) Sleepy sloth: Threads as interrupts as threads. 30th IEEE Real-Time Systems Symposium, Vienna, 29 November-2 December 2011, 67-77.

[4] Dingel, J. (2003) Computer-assisted assume/guarantee reasoning with VeriSoft. Proceedings of the 25th International Conference on Software Engineering (ICSE’03), 138-148.

[5] Joshi, P., Naik, M., Park, C.-S. and Sen, K. (2009) CalFuzzer: An extensible active testing framework for concurrent programs. http://srl.cs.berkeley.edu/~ksen/calfuzzer/

[6] Yang, Y., Chen, X.F., Gopalakrishnan, G. and KirbyInspect, R.M. (2009) A runtime model checker for multithreaded C programs. School of Computing, University of Utah Salt Lake City, Technical Report UT 84112,

[7] 傅修峰, 陈丽容 (2012) 多重中断程序测试框架. 计算机工程与设计, 2, 617-623.

[8] Anderson, Z. (2013) A CIL tutorial-using CIL for language extensions and program analysis. Systems Group Department of Computer Science, ETH Zürich.

[9] Chaki, S., Clarke, E.M., Ouaknine, J., et al. (2004) Automated, compositional and iterative deadlock detection. Proceedings of the 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design, IEEE Press, 201-210.

[10] Flanagan, C. and Godefroid, P. (2005) Dynamic partial-order reduction for model checking software. Proceedings of POPL 2005, Long Beach, ACM Press, 110-121.

[11] Godefroid, P. (1996) Partial-order methods for the verification of concurrent systems—An approach to the state-explosion problem. Springer-Verlag New York, Inc., Secaucus.

[12] Valmari, A. (1991) Stubborn sets for reduced state space generation. In: Lecture Notes in Computer Science, Vol. 483, Advances in Petri Nets 1990, Springer Press, Berlin, 491-515.