Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness

Yanhong A. Liu; Scott D. Stoller

doi:10.1007/978-3-030-60508-7_3

Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

4 Scopus citations

Abstract

This paper presents a general framework and methods for complete programming and checking of distributed algorithms at a high-level, as in pseudocode languages, but precisely specified and directly executable, as in formal specification languages and practical programming languages, respectively. The checking framework, as well as the writing of distributed algorithms and specification of their safety and liveness properties, use DistAlgo, a high-level language for distributed algorithms. We give a complete executable specification of the checking framework, with a complete example algorithm and example safety and liveness properties.

Original language	English
Title of host publication	Runtime Verification - 20th International Conference, RV 2020, Proceedings
Editors	Jyotirmoy Deshmukh, Dejan Nickovic
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	47-66
Number of pages	20
ISBN (Print)	9783030605070
DOIs	https://doi.org/10.1007/978-3-030-60508-7_3
State	Published - 2020
Event	20th International Conference on Runtime Verification, RV 2020 - Los Angeles, United States Duration: Oct 6 2020 → Oct 9 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12399 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	20th International Conference on Runtime Verification, RV 2020
Country/Territory	United States
City	Los Angeles
Period	10/6/20 → 10/9/20

Access to Document

10.1007/978-3-030-60508-7_3

Cite this

Liu, Y. A., & Stoller, S. D. (2020). Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness. In J. Deshmukh, & D. Nickovic (Eds.), Runtime Verification - 20th International Conference, RV 2020, Proceedings (pp. 47-66). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12399 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-60508-7_3

Liu, Yanhong A. ; Stoller, Scott D. / Assurance of Distributed Algorithms and Systems : Runtime Checking of Safety and Liveness. Runtime Verification - 20th International Conference, RV 2020, Proceedings. editor / Jyotirmoy Deshmukh ; Dejan Nickovic. Springer Science and Business Media Deutschland GmbH, 2020. pp. 47-66 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{f048b6ab030a4c9d8344b4311bec08ee,

title = "Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness",

abstract = "This paper presents a general framework and methods for complete programming and checking of distributed algorithms at a high-level, as in pseudocode languages, but precisely specified and directly executable, as in formal specification languages and practical programming languages, respectively. The checking framework, as well as the writing of distributed algorithms and specification of their safety and liveness properties, use DistAlgo, a high-level language for distributed algorithms. We give a complete executable specification of the checking framework, with a complete example algorithm and example safety and liveness properties.",

author = "Liu, \{Yanhong A.\} and Stoller, \{Scott D.\}",

note = "Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 20th International Conference on Runtime Verification, RV 2020 ; Conference date: 06-10-2020 Through 09-10-2020",

year = "2020",

doi = "10.1007/978-3-030-60508-7\_3",

language = "English",

isbn = "9783030605070",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "47--66",

editor = "Jyotirmoy Deshmukh and Dejan Nickovic",

booktitle = "Runtime Verification - 20th International Conference, RV 2020, Proceedings",

}

Liu, YA & Stoller, SD 2020, Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness. in J Deshmukh & D Nickovic (eds), Runtime Verification - 20th International Conference, RV 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12399 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 47-66, 20th International Conference on Runtime Verification, RV 2020, Los Angeles, United States, 10/6/20. https://doi.org/10.1007/978-3-030-60508-7_3

Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness. / Liu, Yanhong A.; Stoller, Scott D.
Runtime Verification - 20th International Conference, RV 2020, Proceedings. ed. / Jyotirmoy Deshmukh; Dejan Nickovic. Springer Science and Business Media Deutschland GmbH, 2020. p. 47-66 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12399 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Assurance of Distributed Algorithms and Systems

T2 - 20th International Conference on Runtime Verification, RV 2020

AU - Liu, Yanhong A.

AU - Stoller, Scott D.

PY - 2020

Y1 - 2020

N2 - This paper presents a general framework and methods for complete programming and checking of distributed algorithms at a high-level, as in pseudocode languages, but precisely specified and directly executable, as in formal specification languages and practical programming languages, respectively. The checking framework, as well as the writing of distributed algorithms and specification of their safety and liveness properties, use DistAlgo, a high-level language for distributed algorithms. We give a complete executable specification of the checking framework, with a complete example algorithm and example safety and liveness properties.

AB - This paper presents a general framework and methods for complete programming and checking of distributed algorithms at a high-level, as in pseudocode languages, but precisely specified and directly executable, as in formal specification languages and practical programming languages, respectively. The checking framework, as well as the writing of distributed algorithms and specification of their safety and liveness properties, use DistAlgo, a high-level language for distributed algorithms. We give a complete executable specification of the checking framework, with a complete example algorithm and example safety and liveness properties.

UR - https://www.scopus.com/pages/publications/85093123214

U2 - 10.1007/978-3-030-60508-7_3

DO - 10.1007/978-3-030-60508-7_3

M3 - Conference contribution

AN - SCOPUS:85093123214

SN - 9783030605070

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 47

EP - 66

BT - Runtime Verification - 20th International Conference, RV 2020, Proceedings

A2 - Deshmukh, Jyotirmoy

A2 - Nickovic, Dejan

PB - Springer Science and Business Media Deutschland GmbH

Y2 - 6 October 2020 through 9 October 2020

ER -

Liu YA , Stoller SD. Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness. In Deshmukh J, Nickovic D, editors, Runtime Verification - 20th International Conference, RV 2020, Proceedings. Springer Science and Business Media Deutschland GmbH. 2020. p. 47-66. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-60508-7_3

Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this