Formal analysis of a real-time kernel specification

被引:0
|
作者
Fowler, S
Wellings, A
机构
关键词
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
The specification of a red-time kernel and the analysis of certain properties of the kernel using the PVS system is presented in this paper. The kernel is designed to provide the minimal functionality to support real-time Ada 95 applications on a uniprocessor system, and the requirements for the kernel are derived from this. The specification consists of an abstract model of the functional and timing requirements for the kernel, and a minimal model of the system that the kernel is do signed to support. This system model allows properties such as mutual exclusion to be proved about the kernel with respect to certain assumptions about the system.
引用
收藏
页码:440 / 458
页数:19
相关论文
共 50 条
  • [41] A formal framework for real-time information flow analysis
    Son, Joon
    Alves-Foss, Jim
    COMPUTERS & SECURITY, 2009, 28 (06) : 421 - 432
  • [42] FORMAL TRAINING ANALYSIS FOR DISTRIBUTED REAL-TIME PROGRAMS
    WEDDE, HF
    KOREL, B
    HUIZINGA, DM
    REAL-TIME SYSTEMS, 1994, 7 (01) : 57 - 90
  • [43] Formal modeling and analysis of real-time resource-sharing protocols in Real-Time Maude
    Olveczky, Peter Csaba
    Prabhakar, Pavithra
    Liu, Xue
    2008 IEEE INTERNATIONAL SYMPOSIUM ON PARALLEL & DISTRIBUTED PROCESSING, VOLS 1-8, 2008, : 3774 - +
  • [44] Formal Analysis of TSN Scheduler for Real-Time Communications
    Lv, Jin
    Zhao, Yongxin
    Wu, Xi
    Li, Yongjian
    Wang, Qiang
    IEEE TRANSACTIONS ON RELIABILITY, 2021, 70 (03) : 1286 - 1294
  • [45] Kernel regression for real-time building energy analysis
    Brown, Matthew
    Barrington-Leigh, Chris
    Brown, Zosia
    JOURNAL OF BUILDING PERFORMANCE SIMULATION, 2012, 5 (04) : 263 - 276
  • [46] Analysis of Linux kernel's real-time performance
    Zhang Yanyan
    Ran Xiangjin
    2018 INTERNATIONAL CONFERENCE ON SMART GRID AND ELECTRICAL AUTOMATION (ICSGEA), 2018, : 191 - 194
  • [47] SPECIFYING A REAL-TIME KERNEL
    SPIVEY, JM
    IEEE SOFTWARE, 1990, 7 (05) : 21 - 28
  • [48] UNIVERSAL REAL-TIME KERNEL
    MANIECKI, M
    MICROPROCESSING AND MICROPROGRAMMING, 1984, 14 (3-4): : 161 - 163
  • [49] The asterix real-time kernel
    Thane, H
    Pettersson, A
    Sundmark, D
    13TH EUROMICRO CONFERENCE ON REAL-TIME SYSTEMS, PROCEEDINGS, 2001, : 33 - 39
  • [50] Spark real-time kernel
    Kotlarsky, Anatoly
    Dr. Dobb's Journal, 1999, 24 (05):