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 条
  • [41] Formal description of time management in real-time operating systems
    Rusu-Banu, Fabricio
    Wang, Yingxu
    [J]. 2006 CANADIAN CONFERENCE ON ELECTRICAL AND COMPUTER ENGINEERING, VOLS 1-5, 2006, : 1801 - +
  • [42] Time- and angle-triggered real-time kernel
    Chabrol, Damien
    Roux, Didier
    David, Vincent
    Jan, Mathieu
    Ait Hmid, Moha
    Oudin, Patrice
    Zeppa, Gilles
    [J]. DESIGN, AUTOMATION & TEST IN EUROPE, 2013, : 1060 - 1062
  • [43] An approach to a synthesis of formal and visual description techniques for the development of real-time reactive systems
    Muthiayen, D
    Alagar, VS
    Khendek, F
    Sefidcon, A
    [J]. SEVENTH INTERNATIONAL CONFERENCE ON REAL-TIME COMPUTING SYSTEMS AND APPLICATIONS, PROCEEDINGS, 2000, : 491 - 497
  • [44] Formal modeling for a real-time scheduler and schedulability analysis
    Kim, SJ
    Choi, JY
    [J]. PARALLEL COMPUTING TECHNOLOGIES, PROCEEDINGS, 2003, 2763 : 253 - 258
  • [45] Formal verification of UML statecharts with real-time extensions
    David, A
    Möller, MO
    Yi, W
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2002, 2306 : 218 - 232
  • [46] Signal: A formal design environment for real-time systems
    LeGuernic, P
    [J]. TAPSOFT '95: THEORY AND PRACTICE OF SOFTWARE DEVELOPMENT, 1995, 915 : 789 - 790
  • [47] Formal verification of real-time systems with preemptive scheduling
    Didier Lime
    Olivier (H. ) Roux
    [J]. Real-Time Systems, 2009, 41 : 118 - 151
  • [48] Formal Analysis of Sporadic Bursts in Real-Time Systems
    Quinton, Sophie
    Negrean, Mircea
    Ernst, Rolf
    [J]. DESIGN, AUTOMATION & TEST IN EUROPE, 2013, : 767 - 772
  • [49] A Formal Approach to Real-Time object oriented sofware
    Carvalho, SE
    Fiadeiro, JL
    Haeusler, EH
    [J]. REAL TIME PROGRAMMING 1997: (WRTP 97), 1998, : 71 - 76
  • [50] A formal design language for real-time systems with data
    Bradley, S
    Henderson, W
    Kendall, D
    Robson, A
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2001, 40 (01) : 3 - 29
12345