Title :
Efficient Integration of Online Model Checking into a Small-Footprint Real-Time Operating System
Author :
Sudhakar, K. ; Yuhong Zhao ; Rammig, Franz-Josef
Author_Institution :
Heinz Nixdorf Inst., Univ. of Paderborn, Paderborn, Germany
Abstract :
In this paper we discuss how an efficient online model checker and a small-footprint RTOS can be integrated. Alternative approaches are discussed, leading to the decision for a federated approach. An implemented prototype is described and some analytical as well as experimental evaluations are presented.
Keywords :
formal verification; operating systems (computers); real-time systems; federated approach; online model checker; online model checking; small-footprint RTOS; small-footprint real-time operating system; Instruction sets; Kernel; Model checking; Monitoring; Real-time systems; Runtime; Online Model Checking; Online verification; QEMU; Real-Time Operating System;
Conference_Titel :
Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC), 2014 IEEE 17th International Symposium on
Conference_Location :
Reno, NV
DOI :
10.1109/ISORC.2014.21
