WEAKEST PRECONDITION SEMANTICS FOR TIME AND CONCURRENCY

被引：3
|
作者：
SCHOLEFIELD, D
ZEDAN, HSM
机构：
[1] Formal Systems Research Group, Department of Computer Science, University of York, Heslington, York
来源：
INFORMATION PROCESSING LETTERS | 1992年 / 43卷 / 06期
关键词：
FORMAL SEMANTICS; WEAKEST PRECONDITIONS; REAL-TIME SYSTEMS; CONCURRENCY;
D O I：
10.1016/0020-0190(92)90116-D
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
A weakest precondition semantics for a real-time concurrent language is defined. An example in verification is presented, and the use of predicate transformers as the basis of a refinement calculus is also discussed.
引用
收藏
页码：301 / 308
页数：8
相关论文
共 46 条
  • [41] Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems
    Dongol, Brijesh
    Derrick, John
    SCIENCE OF COMPUTER PROGRAMMING, 2015, 111 : 214 - 247
  • [42] Time Petri nets with inhibitor hyperarcs. Formal semantics and state space computation
    Roux, OH
    Lime, D
    APPLICATIONS AND THEORY OF PETRI NETS 2004, PROCEEDINGS, 2004, 3099 : 371 - 390
  • [43] A Distributed Real-time Control System Modeling and XNM-based semantics
    Zhang Jing
    Zhang Yunsheng
    Zhang Jiang
    Chen Hao
    Zhang Changsheng
    xiang Fenghong
    2006 CHINESE CONTROL CONFERENCE, VOLS 1-5, 2006, : 1133 - +
  • [44] ENERGY-EFFICIENT CONCURRENCY CONTROL FOR DYNAMIC-PRIORITY REAL-TIME TASKS WITH ABORTABLE CRITICAL SECTIONS
    Wu, Jun
    COMPUTING AND INFORMATICS, 2017, 36 (04) : 765 - 792
  • [45] A POLYNOMIAL-TIME ALGORITHM TO DECIDE PAIRWISE CONCURRENCY OF TRANSITIONS FOR 1-BOUNDED CONFLICT-FREE PETRI NETS
    YEN, HC
    INFORMATION PROCESSING LETTERS, 1991, 38 (02) : 71 - 76
  • [46] Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking
    Gnesi, S
    Latella, D
    Massink, M
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2002, 51 (01): : 43 - 75
12345