Formal analysis of a real-time kernel specification

被引：0
作者：
Fowler, S
Wellings, A
机构：
来源：
FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS | 1996年 / 1135卷
关键词：
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
相关论文
共 16 条
  • [1] [Anonymous], 1995, WIFT 95 WORKSH IND S
  • [2] APPLYING NEW SCHEDULING THEORY TO STATIC PRIORITY PREEMPTIVE SCHEDULING
    AUDSLEY, N
    BURNS, A
    RICHARDSON, M
    TINDELL, K
    WELLINGS, AJ
    [J]. SOFTWARE ENGINEERING JOURNAL, 1993, 8 (05): : 284 - 292
  • [3] BEVIER WR, 1988, 28 COMP LOG INC
  • [4] BURNS A, 1991, ADA USER, V12, P160
  • [5] BURNS A, 1995, CONCURRENCY ADA
  • [6] FIDGE C, 1994, 9411 U QUEENSL DEP C
  • [7] FOWLER S, 1996, 265 YCS U YORK DEP C
  • [8] Gorski J., 1994, Proceedings Sixth Euromicro Workshop on Real-Time Systems, P205, DOI 10.1109/EMWRTS.1994.336841
  • [9] *INT INC, 1995, 8652 ISO IEC
  • [10] SAFETY ANALYSIS OF TIMING PROPERTIES IN REAL-TIME SYSTEMS
    JAHANIAN, F
    MOK, AK
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1986, 12 (09) : 890 - 904
12