Efficient Integration of Online Model Checking into a Small-Footprint Real-time Operating System

被引:0
|
作者
Sudhakar, Krishna [1 ]
Zhao, Yuhong [1 ]
Rammig, Franz-Josef [1 ]
机构
[1] Univ Paderborn, Heinz Nixdorf Inst, D-33098 Paderborn, Germany
关键词
Online Verification; Online Model Checking; Real-time Operating System; and QEMU;
D O I
10.1109/ISORC.2014.21
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
In this paper we discuss how an efficient online model checker and a small-footprint RTOS can be integrated. Alternative integration approaches are discussed, leading to the decision for a federated approach. An implemented prototype is described and some analytical as well as experimental evaluation are presented.
引用
收藏
页码:374 / 383
页数:10
相关论文
共 50 条
  • [1] Efficient integration of online model checking into a small-footprint real-time operating system
    Sudhakar, Krishna
    Zhao, Yuhong
    Rammig, Franz-Josef
    CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2016, 28 (14): : 3773 - 3797
  • [2] Correctness of efficient real-time model checking
    Reif, W
    Schellhorn, G
    Vollmer, T
    Ruf, J
    JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2001, 7 (02) : 194 - 209
  • [3] An efficient algorithm for real-time symbolic model checking
    Frossl, J
    Gerlach, J
    Kropf, T
    EUROPEAN DESIGN & TEST CONFERENCE 1996 - ED&TC 96, PROCEEDINGS, 1996, : 15 - 20
  • [4] Efficient CTMC Model Checking of Linear Real-Time Objectives
    Barbot, Benoit
    Chen, Taolue
    Han, Tingting
    Katoen, Joost-Pieter
    Mereacre, Alexandru
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2011, 6605 : 128 - +
  • [5] Efficient Model-Checking for Real-Time Task Networks
    Dierks, Henning
    Metzner, Alexander
    Stierand, Ingo
    2009 INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE AND SYSTEMS, PROCEEDINGS, 2009, : 11 - 18
  • [6] Model checking multi-task software on real-time operating systems
    Aoki, Toshiaki
    ISORC 2008: 11TH IEEE SYMPOSIUM ON OBJECT/COMPONENT/SERVICE-ORIENTED REAL-TIME DISTRIBUTED COMPUTING - PROCEEDINGS, 2008, : 551 - 555
  • [7] Model Checking Multitask Applications for OSEK Compliant Real-Time Operating Systems
    McKelvin, Mark L., Jr.
    Gamble, Edward B., Jr.
    Holzmann, Gerard J.
    2011 IEEE 17TH PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING (PRDC), 2011, : 280 - 281
  • [8] SIMULATION OF REAL-TIME MINICOMPUTER OPERATING SYSTEM MODEL
    ROOTENBERG, J
    TANNENBAUM, L
    INTERNATIONAL JOURNAL OF SYSTEMS SCIENCE, 1977, 8 (05) : 547 - 560
  • [9] Operating system structure model for real-time systems
    Kamiuchi, T
    Nakanishi, H
    Hayashi, K
    SECOND WORKSHOP ON OBJECT-ORIENTED REAL-TIME DEPENDABLE SYSTEMS, PROCEEDINGS OF WORDS '96, 1996, : 120 - 124
  • [10] REAL-TIME OPERATING SYSTEM
    HANATA, S
    MUKOZAKA, H
    YAMAZAKI, H
    REVIEW OF THE ELECTRICAL COMMUNICATIONS LABORATORIES, 1975, 23 (9-10): : 1027 - 1036