Fairness in Temporal Verification of Distributed Systems
Wiktor B. Daszczuk
AbstractThe 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.
|Publication size in sheets||0.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 English||Distributed system specification, model checking, deadlock and termination detection, strong fairness, compassion|
|Publication indicators||= 2|
|Citation count*||2 (2019-09-09)|
* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.