Fairness in Temporal Verification of Distributed Systems

Wiktor B. Daszczuk

Abstract

The verification of deadlock freeness and distributed termination in distributed systems by Dedan tool is described. In Dedan, the IMDS formalism for specification of distributed systems is used. A system is described in terms of servers’ states, agents’ messages, and actions. Universal temporal formulas for checking deadlock and termination features are elaborated. It makes possi-ble to verify distributed systems without a knowledge of temporal logic by a us-er. For verification, external model checkers: Spin, NuSMV and Uppaal are used. The experience with these verifiers show problems with strong fairness (compassion), required for model checking of distributed systems. These prob-lems outcome from busy form of waiting in some examples. The problem is solved by own temporal formulas evaluation algorithm, using breadth-first search and reverse reachability. This algorithm does not require to specify com-passion requirements for individual events, as it supports strong fairness for all cases. Thus it is appropriate for verification of distributed systems.
Author Wiktor B. Daszczuk (FEIT / IN)
Wiktor B. Daszczuk,,
- The Institute of Computer Science
Pages135-150
Publication size in sheets0.75
Book Zamojski Wojciech, Mazurkiewicz Jacek, Sugier Jarosław, Walkowiak Tomasz (eds.): Contemporary Complex Systems and Their Dependability. Proceedings of the Thirteenth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX, Advances in Intelligent Systems and Computing, vol. 761, 2019, Springer International Publishing, ISBN 978-3-319-91445-9, [978-3-319-91446-6], 566 p., DOI:10.1007/978-3-319-91446-6
Keywords in EnglishDistributed system specification, model checking, deadlock and termination detection, strong fairness, compassion
DOIDOI:10.1007/978-3-319-91446-6_14
URL https://www.springer.com/us/book/9783319914459#aboutBook
Languageen angielski
File
Fairness_Depcos_8.pdf 1.22 MB
Score (nominal)0
Publication indicators Scopus Citations = 2
Citation count*2 (2019-09-09)
Cite
Share Share

Get link to the record


* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.
Back