Formalizing real-time scheduling as program refinement

被引:0
|
作者
Liu, ZM [1 ]
Joseph, M
机构
[1] Univ Leicester, Dept Math & Comp Sci, Leicester LE1 7RH, Leics, England
[2] Univ Warwick, Dept Comp Sci, Coventry CV4 7AL, W Midlands, England
关键词
real-time program; specification; refinement; feasibility;
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
This paper shows how the feasibility of scheduling a realtime program consisting of a number of parallel processes (tasks) can be proved as a step in the refinement of the program from its specification. Verification of this step of refinement makes formal use of methods and results from real-time scheduling theory.
引用
收藏
页码:295 / 309
页数:15
相关论文
共 50 条
  • [1] Formalizing hierarchical scheduling for refinement of real-time systems
    Zhu, Chenyang
    Butler, Michael
    Cirstea, Corina
    SCIENCE OF COMPUTER PROGRAMMING, 2020, 189
  • [2] Verification, refinement and scheduling of real-time programs
    Liu, ZM
    Joseph, M
    THEORETICAL COMPUTER SCIENCE, 2001, 253 (01) : 119 - 152
  • [3] Procedures and parameters in the real-time program refinement calculus
    Hayes, Ian J.
    SCIENCE OF COMPUTER PROGRAMMING, 2007, 64 (03) : 286 - 311
  • [4] Real-time program refinement using auxiliary variables
    Hayes, I
    FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, PROCEEDINGS, 2000, 1926 : 170 - 184
  • [5] Formalizing Real-Time Embedded System into Promela
    Sukvanich, Punwess
    Thongtak, Arthit
    Vatanawood, Wiwat
    2015 4TH INTERNATIONAL CONFERENCE ON MECHANICS AND CONTROL ENGINEERING (ICMCE 2015), 2015, 35
  • [6] Real-time calculus for scheduling hard real-time systems
    Thiele, L
    Chakraborty, S
    Naedele, M
    ISCAS 2000: IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS - PROCEEDINGS, VOL IV: EMERGING TECHNOLOGIES FOR THE 21ST CENTURY, 2000, : 101 - 104
  • [7] Refinement of infeasible real-time programs
    Utting, M
    Fidge, C
    FORMAL METHODS PACIFIC '97, 1997, : 243 - 262
  • [8] A sequential real-time refinement calculus
    Hayes, IJ
    Utting, M
    ACTA INFORMATICA, 2001, 37 (06) : 385 - 448
  • [9] A sequential real-time refinement calculus
    Ian J. Hayes
    Mark Utting
    Acta Informatica, 2001, 37 : 385 - 448
  • [10] SCHEDULING IN REAL-TIME MODELS
    KURKISUONIO, R
    SYSTA, K
    VAIN, J
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 571 : 327 - 339