关键词: 嵌入式操作系统, 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