• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

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

• 论文 • Previous Articles     Next Articles

A runtime verification method for
embedded operating system          

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

  1. (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:

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