一种嵌入式操作系统运行时验证方法

J4 ›› 2014, Vol. 36 ›› Issue (05): 900-905.

一种嵌入式操作系统运行时验证方法

张可迪,舒绍娴,董威

（国防科学技术大学计算机学院，湖南长沙 410073)

收稿日期:2012-11-09 修回日期:2013-04-17 出版日期:2014-05-25 发布日期:2014-05-25
基金资助:
国家自然科学基金资助项目（60970035）；国家863计划资助项目（2011AA010106）

A runtime verification method for
embedded operating system

ZHANG Kedi,SHU Shaoxian,DONG Wei

(College of Computer,National University of Defense Technology,Changsha 410073,China)

Received:2012-11-09 Revised:2013-04-17 Online:2014-05-25 Published:2014-05-25

摘要/Abstract

摘要：

作为测试、模型检验等开发阶段所用技术的有效补充，运行时验证技术越来越受到广泛的关注。然而，当前的运行时验证技术主要用于应用软件，很少专门针对操作系统进行研究。对面向嵌入式操作系统的运行时验证框架和关键技术进行了研究，并结合一个开源嵌入式操作系统FreeRTOS进行了设计与实现。首先提出了一种面向嵌入式操作系统的运行时验证和反馈调整框架，然后针对框架中的关键技术部分，完成了规约语言的设计、三值语义监控器的生成、FreeRTOS嵌入式操作系统相关接口的实现等主要工作。

关键词: 嵌入式操作系统, FreeRTOS, 运行时验证, 规约语言, 三值语义监控器

Abstract:

As an effective supplement of testing and model checking, runtime verification technique attracts more and more attentions. However, the current runtime verification technology is mainly used for application software. Very few are specialized for monitoring the running state of an operating system. The paper studies the runtime verification framework and key techniques for embedded operating system and realizes a demo combined with an open source system FreeRTOS. Firstly, an embedded operating system oriented framework for runtime verification and feedback adjustment is proposed. Secondly, based on the critical part of our frame, the specification language, threevalued semantic monitor generation and FreeRTOS related interfaces are designed and implemented.

Key words: embedded operating system;FreeRTOS;runtime verification;specification language;threevalued semantic monitor

张可迪,舒绍娴,董威. 一种嵌入式操作系统运行时验证方法[J]. J4, 2014, 36(05): 900-905.

ZHANG Kedi,SHU Shaoxian,DONG Wei. A runtime verification method for
embedded operating system [J]. J4, 2014, 36(05): 900-905.

参考文献

［1］Colin S, Mariani L. Runtime verification, chapter 18 ［J］. Proc of LNCS,2005, 3472:525555.
［2］Peleska J.Test automation for safetycritical systems:Industrial application and future developments［C］∥Proc of the 3rd International Symposium of Formal Methods,1996,1051:3959.
［3］Clarke E M,Grumberg O,Peled D A. Model checking［M］.London:The MIT Press,1999.
［4］Liu Bin, Wang Qi, Liu Lili.Principle and implementation of embedded operating system FreeRTOS［J］.Mocrocontroller and Embedded System,2005(7):12.(in Chinese)
［5］Kroger F. The temporal logic of programs［M］.NewYork:SpringerVerlag,1987.
［6］Sammapun U,Lee I, Sokolsky O. RTMaC:Runtime monitoring and checking of quantitative and probabilistic properties［C］∥Proc of the 11th IEEE International Conference of Embedded and RealTime Computing Systems and Applications,2005:147153.
［7］Kim M, Kannan S, Lee I, et al. JavaMaC:A runtime assurance approach for Java programs［J］.Formal Methods in Systems Design, 2004,24(2):129155.
［8］MaC Research team of Univeristy of Pennsylvania.Languages in the MaC prototype implementation［EB/OL］.［20080101］.http://rtg.cis.upenn.edu/mac/index.php3.
［9］Barry R. FreeRTOS user manual［EB/OL］.［20041209］.http://www.FreeRTOS.net.
［10］Geilen M C W. On the construction of monitors for temporal logic properties［J］. Electronic Notes in Theoretical Computer Science,2001,55(2):181199.
［11］Bauer A,Leucher M,Schallhart C.Runtime verification for LTL and PTLTL［J］. Journal of ACM Transactions on Sotware Engineer and Methodology, 2011,20(4):Article No.14.
［12］Sui Ping.Software runtime verification method based on threevalued semantics［D］.Changsha:National University of Defense Technology,2010.(in Chinese)
附中文参考文献:
［4］刘滨,王琦,刘丽丽.嵌入式操作系统FreeRTOS的原理与实现［J］.单片机与嵌入式系统应用,2005(7):12.
［12］隋平.基于三值语义的软件运行时验证方法.［D］.长沙：国防科学技术大学,2010.

[1]	张小艳，文辉. 基于ASL的模型驱动架构测试方法[J]. J4, 2014, 36(04): 662-666.
[2]	隋〓平1,赵常智1,董〓威1,李冰鹏2. 基于三值语义的软件运行时验证方法[J]. J4, 2011, 33(10): 99-104.
[3]	肖来元赵吉军. VxWorks下USB驱程栈框架模型及其应用研究[J]. J4, 2007, 29(3): 94-96.
[4]	冯翔[1] 李仁发[1] 喻飞[2] 易非[1]. 嵌入式Linux中闪存设备驱动程序开发[J]. J4, 2005, 27(3): 96-98.
[5]	谢长生杜胜军. 基于Nucleus的窗口小控件的实现[J]. J4, 2004, 26(4): 30-31.
[6]	钟汉如王创生. 嵌入式Linux中调度算法的实现及优化[J]. J4, 2002, 24(3): 5-7.