Adding the leads-to operator to Dijkstrais calculus

被引：3
|
作者：
Singh, AK [1 ]
Bandyopadhyay, AK
机构：
[1] Natl Inst Technol, Dept Comp Engn, Kurukshetra 136119, Haryana, India
[2] Jadavpur Univ, Dept Elect & Telecommun Engn, Kolkata 700032, W Bengal, India
来源：
ACM SIGPLAN NOTICES | 2004年 / 39卷 / 02期
关键词：
weakest precondition; guarded process; non-deterministic selection; protocol; weakest cooperation; correctness;
D O I：
10.1145/967278.967282
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
A temporal operator, namely leads-to, has been incorporated into the Dijkstrais weakest precondition calculus. It is demonstrated that the augmented calculus provides a basis, not only for the modeling but also, for a straightforward and thorough analysis of large and complex distributed systems. The technique has been illustrated by describing a data link layer protocol. This analysis contributes to the understanding of the system.
引用
收藏
页码：12 / 17
页数：6
相关论文
共 50 条
  • [1] Composing leads-to properties
    Meier, D
    Sanders, B
    THEORETICAL COMPUTER SCIENCE, 2000, 243 (1-2) : 339 - 361
  • [2] ELIMINATING DISJUNCTIONS OF LEADS-TO PROPERTIES
    CALVERT, K
    INFORMATION PROCESSING LETTERS, 1994, 49 (04) : 189 - 194
  • [3] Natural product scaffolds as leads-to drugs
    Newman, David J.
    Cragg, Gordon M.
    FUTURE MEDICINAL CHEMISTRY, 2009, 1 (08) : 1415 - 1427
  • [4] A Divide & Conquer Approach to Leads-to Model Checking
    Phyo, Yati
    Do, Canh Minh
    Ogata, Kazuhiro
    COMPUTER JOURNAL, 2022, 65 (06): : 1353 - 1364
  • [5] Calculating and composing progress properties in terms of the leads-to relation
    Mooij, Arjan J.
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2007, 4789 : 366 - 386
  • [6] A SIMPLE PROOF OF A COMPLETENESS RESULT FOR LEADS-TO IN THE UNITY LOGIC
    PACHL, J
    INFORMATION PROCESSING LETTERS, 1992, 41 (01) : 35 - 38
  • [7] Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way
    Canh Minh Do
    Phyo, Yati
    Riesco, Adrian
    Ogata, Kazuhiro
    ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2023, 32 (06)
  • [8] Verification and Synthesis of Symmetric Uni-Rings for Leads-To Properties
    Ebnenasir, Ali
    2019 FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD), 2019, : 78 - 86
  • [9] OPERATOR CALCULUS
    FEINSILVER, P
    PACIFIC JOURNAL OF MATHEMATICS, 1978, 78 (01) : 95 - 116
  • [10] OPERATOR CALCULUS OF QUANTIZED OPERATOR
    FUJIWARA, I
    PROGRESS OF THEORETICAL PHYSICS, 1952, 7 (05): : 433 - 448
12345