Complete assertional proof rules for progress under weak and strong fairness

Wim H. Hesselink

doi:10.1016/j.scico.2012.10.013

Complete assertional proof rules for progress under weak and strong fairness

Wim H. Hesselink

Research output: Contribution to journal › Article › Academic › peer-review

3 Citations (Scopus)

Abstract

The UNITY rules for leads-to, based on totality of the commands and weak fairness, are generalized to specifications with nontotal commands and impartiality. The rules and the corresponding predicate transformers are proved to be sound and complete by elementary means. These results are subsequently extended to specifications where the liveness property also contains a finite number of strong fairness assumptions. This is illustrated by means of a proof of starvation freedom for the standard implementation of mutual exclusion by plain semaphores, with strong fairness for the P operations. (C) 2012 Elsevier B.V. All rights reserved.

Original language	English
Pages (from-to)	1521-1537
Number of pages	17
Journal	Science of computer programming
Volume	78
Issue number	9
DOIs	https://doi.org/10.1016/j.scico.2012.10.013
Publication status	Published - 1-Sept-2013

Keywords

UNITY
Temporal logic
Weak fairness
Strong fairness
Proof rules
UNITY LOGIC
PROGRAMS
DERIVATION
REFINEMENT
SYSTEM

Access to Document

10.1016/j.scico.2012.10.013

Handle.net

Persistent link

Embargoed Document

2013SciComputProgHesselink1.pdf
Final publisher's version, 324 KB

Cite this

@article{8d73fc8ab815445d882ab2a7eb909796,

title = "Complete assertional proof rules for progress under weak and strong fairness",

abstract = "The UNITY rules for leads-to, based on totality of the commands and weak fairness, are generalized to specifications with nontotal commands and impartiality. The rules and the corresponding predicate transformers are proved to be sound and complete by elementary means. These results are subsequently extended to specifications where the liveness property also contains a finite number of strong fairness assumptions. This is illustrated by means of a proof of starvation freedom for the standard implementation of mutual exclusion by plain semaphores, with strong fairness for the P operations. (C) 2012 Elsevier B.V. All rights reserved.",

keywords = "UNITY, Temporal logic, Weak fairness, Strong fairness, Proof rules, UNITY LOGIC, PROGRAMS, DERIVATION, REFINEMENT, SYSTEM",

author = "Hesselink, {Wim H.}",

note = "Relation: http://www.rug.nl/research/jbi/ Rights: University of Groningen, Johann Bernoulli Institute for Mathematics and Computer Science",

year = "2013",

month = sep,

day = "1",

doi = "10.1016/j.scico.2012.10.013",

language = "English",

volume = "78",

pages = "1521--1537",

journal = "Science of computer programming",

issn = "0167-6423",

publisher = "ELSEVIER SCIENCE BV",

number = "9",

}

TY - JOUR

T1 - Complete assertional proof rules for progress under weak and strong fairness

AU - Hesselink, Wim H.

N1 - Relation: http://www.rug.nl/research/jbi/ Rights: University of Groningen, Johann Bernoulli Institute for Mathematics and Computer Science

PY - 2013/9/1

Y1 - 2013/9/1

N2 - The UNITY rules for leads-to, based on totality of the commands and weak fairness, are generalized to specifications with nontotal commands and impartiality. The rules and the corresponding predicate transformers are proved to be sound and complete by elementary means. These results are subsequently extended to specifications where the liveness property also contains a finite number of strong fairness assumptions. This is illustrated by means of a proof of starvation freedom for the standard implementation of mutual exclusion by plain semaphores, with strong fairness for the P operations. (C) 2012 Elsevier B.V. All rights reserved.

AB - The UNITY rules for leads-to, based on totality of the commands and weak fairness, are generalized to specifications with nontotal commands and impartiality. The rules and the corresponding predicate transformers are proved to be sound and complete by elementary means. These results are subsequently extended to specifications where the liveness property also contains a finite number of strong fairness assumptions. This is illustrated by means of a proof of starvation freedom for the standard implementation of mutual exclusion by plain semaphores, with strong fairness for the P operations. (C) 2012 Elsevier B.V. All rights reserved.

KW - UNITY

KW - Temporal logic

KW - Weak fairness

KW - Strong fairness

KW - Proof rules

KW - UNITY LOGIC

KW - PROGRAMS

KW - DERIVATION

KW - REFINEMENT

KW - SYSTEM

U2 - 10.1016/j.scico.2012.10.013

DO - 10.1016/j.scico.2012.10.013

M3 - Article

SN - 0167-6423

VL - 78

SP - 1521

EP - 1537

JO - Science of computer programming

JF - Science of computer programming

IS - 9

ER -

Complete assertional proof rules for progress under weak and strong fairness

Abstract

Keywords

Access to Document

Handle.net

Embargoed Document

Fingerprint

Cite this