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 条
  • [21] A relaxed temporal consistency approach for real-time concurrency control
    Lee Ibarra, Alejandro
    Gutierrez Diaz de Leon, Luis A.
    CERMA2006: ELECTRONICS, ROBOTICS AND AUTOMOTIVE MECHANICS CONFERENCE, VOL 1, PROCEEDINGS, 2006, : 274 - +
  • [22] A new time extension to π-calculus based on time consuming transition semantics
    Fischer, M
    Förster, S
    Windisch, A
    Monjau, D
    Balser, B
    LANGUAGES FOR SYSTEM SPECIFICATION: SELECTED CONTRIBUTIONS ON UML, SYSTEMC, SYSTEM VERILOG, MIXED-SIGNAL SYSTEMS, AND PROPERTY SPECIFICATION FROM FDL'03, 2004, : 271 - 283
  • [23] Combining Time and Concurrency in Model-Based Statistical Testing of Embedded Real-Time Systems
    Homm, Daniel
    Eckert, Juergen
    German, Reinhard
    SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2015), 2015, 9509 : 22 - 31
  • [24] Simulating concurrency control with deadlock avoidance in real-time transaction processing
    Department of Computer Science, University of Northern British Columbia, 3333 University Way, Prince George, BC V2N 4Z9, Canada
    Int J Modell Simul, 2007, 2 (131-142): : 131 - 142
  • [25] AN EFFICIENT REAL-TIME CONCURRENCY CONTROL PROTOCOL FOR GUARANTEEING TEMPORAL CONSISTENCY
    Xiao, YingYuan
    Chen, Yueguo
    Lue, Kevin
    Liu, Yunsheng
    INTERNATIONAL JOURNAL OF INNOVATIVE COMPUTING INFORMATION AND CONTROL, 2010, 6 (08): : 3519 - 3527
  • [26] A concurrency-preserving translation from time Petri nets to networks of timed automata
    Balaguer, Sandie
    Chatain, Thomas
    Haar, Stefan
    FORMAL METHODS IN SYSTEM DESIGN, 2012, 40 (03) : 330 - 355
  • [27] A concurrency-preserving translation from time Petri nets to networks of timed automata
    Sandie Balaguer
    Thomas Chatain
    Stefan Haar
    Formal Methods in System Design, 2012, 40 : 330 - 355
  • [28] Reusable formal models for concurrency and communication in custom real-time operating systems
    Adelt, Julius
    Gebker, Julian
    Herber, Paula
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2024, 26 (02) : 229 - 245
  • [29] Reusable formal models for concurrency and communication in custom real-time operating systems
    Julius Adelt
    Julian Gebker
    Paula Herber
    International Journal on Software Tools for Technology Transfer, 2024, 26 : 229 - 245
  • [30] An Operational Semantics of Real-Time Process Algebra (RTPA)
    Wang, Yingxu
    Ngolah, Cyprian F.
    INTERNATIONAL JOURNAL OF COGNITIVE INFORMATICS AND NATURAL INTELLIGENCE, 2008, 2 (03) : 71 - 89
12345