VXWORKS系统并发程序动态测试工具设计
The Design of Dynamic Checking Tool for VXWORKS Systems Concurrent Program

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

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

摘要:

近年来随着实时嵌入式系统自动化程度的不断提升,其设计复杂度不断加大,在设计中大量的使用了并发程序设计方法。但在实时嵌入式系统测试的过程中,由于实时嵌入式系统中中断和线程相互交叠,始终缺乏有效的并发程序测试工具。为此本文设计了针对VXWORKS系统并发程序动态测试工具,提出以标记迁移系统作为并发程序的系统模型,对常见的并发错误给出了形式化定义,使用偏序化简算法缩减程序的状态空间,实现了对多线程、多重中断的并发程序错误检测。

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.

分享
Top