Towards a refinement calculus for concurrent real-time programs

被引:0
|
作者
Peuker, S [1 ]
Hayes, I
机构
[1] Univ Queensland, Software Verificat Res Ctr, St Lucia, Qld 4067, Australia
[2] Univ Queensland, Sch Informat Technol & Elect Engn, St Lucia, Qld 4067, Australia
关键词
D O I
暂无
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
We define a language and a predicative semantics to model concurrent real-time programs. We consider different communication paradigms between the concurrent components of a program: communication via shared variables and asynchronous message passing (for different models of channels). The semantics is the basis for a refinement calculus to derive machine-independent concurrent real-time programs from specifications. We give some examples of refinement laws that deal with concurrency.
引用
收藏
页码:335 / 346
页数:12
相关论文
共 50 条
  • [31] Causality problem in real-time calculus
    Altisen, Karine
    Moy, Matthieu
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2016, 48 (1-2) : 1 - 45
  • [32] Causality problem in real-time calculus
    Karine Altisen
    Matthieu Moy
    [J]. Formal Methods in System Design, 2016, 48 : 1 - 45
  • [33] REAL-TIME AND THE MU-CALCULUS
    EMERSON, EA
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 600 : 176 - 194
  • [34] Multiprocessor extensions to real-time calculus
    Leontyev, Hennadiy
    Chakraborty, Samarjit
    Anderson, James H.
    [J]. REAL-TIME SYSTEMS, 2011, 47 (06) : 562 - 617
  • [35] Multiprocessor extensions to real-time calculus
    Hennadiy Leontyev
    Samarjit Chakraborty
    James H. Anderson
    [J]. Real-Time Systems, 2011, 47 : 562 - 617
  • [36] Generalized Finitary Real-Time Calculus
    Lampka, Kai
    Bondorf, Steffen
    Schmitt, Jens B.
    Guan, Nan
    Yi, Wang
    [J]. IEEE INFOCOM 2017 - IEEE CONFERENCE ON COMPUTER COMMUNICATIONS, 2017,
  • [37] Multiprocessor Extensions to Real-Time Calculus
    Leontyev, Hennadiy
    Chakraborty, Samarjit
    Anderson, James H.
    [J]. 2009 30TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2009, : 410 - +
  • [38] Refinement for Structured Concurrent Programs
    Kragl, Bernhard
    Qadeer, Shaz
    Henzinger, Thomas A.
    [J]. COMPUTER AIDED VERIFICATION (CAV 2020), PT I, 2020, 12224 : 275 - 298
  • [39] REAL-TIME BEHAVIOR OF PROGRAMS
    HAASE, VH
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1981, 7 (05) : 494 - 501
  • [40] TOWARDS A CALCULUS OF DATA REFINEMENT
    CHEN, W
    UDDING, JT
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1989, 375 : 197 - 218