Formal development of a real-time kernel

被引：5
|
作者：
Fowler, S [1 ]
Wellings, A [1 ]
机构：
[1] Univ York, Dept Comp Sci, Real Time Syst Res Grp, York YO1 5DD, N Yorkshire, England
来源：
18TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS | 1997年
关键词：
D O I：
10.1109/REAL.1997.641284
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
The formal development of a simple real-time operating system kernel is described in this paper. The kernel provides a set of operations that allows a restricted Ada 95 tasking model to be supported, suitable for fixed priority real-time systems. The requirements for the kernel are expressed in terms of the computational model using RTL, and the abstract specification of the kernel is validated against this. The development of an implementation from this specification is then described, with the PVS proof system used to verify each step in the development process.
引用
收藏
页码：220 / 229
页数：10
相关论文
共 50 条
  • [1] Formal analysis of a real-time kernel specification
    Fowler, S
    Wellings, A
    [J]. FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, 1996, 1135 : 440 - 458
  • [2] Transformational formal development of real-time systems
    Lano, K
    Sanchez, A
    [J]. TRANSFORMATION-BASED REACTIVE SYSTEMS DEVELOPMENT, 1997, 1231 : 184 - 198
  • [3] REAL-TIME SOFTWARE-DEVELOPMENT WITH FORMAL MODELS
    BAUGH, JW
    ELSEAIDY, WM
    [J]. JOURNAL OF COMPUTING IN CIVIL ENGINEERING, 1995, 9 (01) : 73 - 86
  • [4] SPECIFYING A REAL-TIME KERNEL
    SPIVEY, JM
    [J]. IEEE SOFTWARE, 1990, 7 (05) : 21 - 28
  • [5] REAL-TIME KERNEL INTERFACES
    STANKOVIC, JA
    [J]. REAL-TIME SYSTEMS, 1993, 5 (01) : 5 - 8
  • [6] UNIVERSAL REAL-TIME KERNEL
    MANIECKI, M
    [J]. MICROPROCESSING AND MICROPROGRAMMING, 1984, 14 (3-4): : 161 - 163
  • [7] The asterix real-time kernel
    Thane, H
    Pettersson, A
    Sundmark, D
    [J]. 13TH EUROMICRO CONFERENCE ON REAL-TIME SYSTEMS, PROCEEDINGS, 2001, : 33 - 39
  • [8] Scalability in a real-time kernel
    Oikawa, S
    Rajkumar, R
    [J]. FOURTH INTERNATIONAL WORKSHOP ON REAL-TIME COMPUTING SYSTEMS AND APPLICATIONS, PROCEEDINGS, 1997, : 35 - 42
  • [9] TAM - A FORMAL FRAMEWORK FOR THE DEVELOPMENT OF DISTRIBUTED REAL-TIME SYSTEMS
    SCHOLEFIELD, DJ
    ZEDAN, HSM
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 571 : 411 - 428
  • [10] A new kernel approach for modular real-time systems development
    Gai, P
    Abeni, L
    Giorgi, M
    Buttazzo, G
    [J]. 13TH EUROMICRO CONFERENCE ON REAL-TIME SYSTEMS, PROCEEDINGS, 2001, : 199 - 206
12345