Skip to main content
SpringerLink
Log in
Book cover

International Conference on Dependability and Complex Systems

DepCoS-RELCOMEX 2018: Contemporary Complex Systems and Their Dependability pp 135–150Cite as

Fairness in Temporal Verification of Distributed Systems

  • Conference paper
  • First Online:

Part of the book series: Advances in Intelligent Systems and Computing ((AISC,volume 761))

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 possible to verify distributed systems without a knowledge of temporal logic by a user. 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. The problems 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 compassion requirements for individual events, as it supports strong fairness for all cases. Thus it is appropriate for verification of distributed systems.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Chrobot, S., Daszczuk, W.B.: Communication dualism in distributed systems with petri net interpretation. Theor. Appl. Inform. 18, 261–278 (2006). arXiv: 1710.07907

    Google Scholar 

  2. Daszczuk, W.B.: Communication and resource deadlock analysis using IMDS formalism and model checking. Comput. J. 60, 729–750 (2017). https://doi.org/10.1093/comjnl/bxw099

    Article  Google Scholar 

  3. Dedan. http://staff.ii.pw.edu.pl/dedan/files/DedAn.zip

  4. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008). ISBN 9780262026499

    MATH  Google Scholar 

  5. Ben-Ari, M.: Principles of the Spin Model Checker. Springer, London (2008). https://doi.org/10.1007/978-1-84628-770-1

    Book  MATH  Google Scholar 

  6. Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an OpenSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. Computer Aided Verification. LNCS, vol. 2404, Copenhagen, Denmark, 27–31 July 2002, pp. 359–364. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_29

    Chapter  Google Scholar 

  7. Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing UPPAAL over 15 years. Softw. Pract. Exp. 41, 133–142 (2011). https://doi.org/10.1002/spe.1006

    Article  Google Scholar 

  8. Daszczuk, W.B.: Evaluation of temporal formulas based on “checking by spheres.” In: Proceedings Euromicro Symposium on Digital Systems Design, Warsaw, Poland, 4–6 September 2001, pp. 158–164. IEEE (2001). https://doi.org/10.1109/dsd.2001.952267

  9. Dedan Examples. http://staff.ii.pw.edu.pl/dedan/files/examples.zip

  10. Pnueli, A., Sa’ar, Y.: All you need is compassion. In: 9th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2008, San Francisco, CA, 7–9 January 2008, pp. 233–247. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78163-9_21

  11. Gómez, R., Bowman, H.: Discrete timed automata. Technical report 3-05-2005, Canterbury, UK (2005). https://kar.kent.ac.uk/14362/1/TR305.pdf

  12. Bérard, B.: An introduction to timed automata. In: Control of Discrete-Event Systems, pp. 169–187. Springer, London (2013). https://doi.org/10.1007/978-1-4471-4276-8_9

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Warsaw University of Technology, Nowowiejska Str. 15/19, 00-665, Warsaw, Poland

    Wiktor B. Daszczuk

Authors
  1. Wiktor B. Daszczuk
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wiktor B. Daszczuk .

Editor information

Editors and Affiliations

  1. Department of Computer Engineering, Wrocław University of Technology, Wrocław, Poland

    Wojciech Zamojski

  2. Department of Computer Engineering, Wrocław University of Technology, Wrocław, Poland

    Jacek Mazurkiewicz

  3. Department of Computer Engineering, Wrocław University of Technology, Wrocław, Poland

    Jarosław Sugier

  4. Department of Computer Engineering, Wrocław University of Technology, Wrocław, Poland

    Tomasz Walkowiak

  5. Polish Academy of Sciences, Systems Research Institute, Warsaw, Poland

    Janusz Kacprzyk

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Daszczuk, W.B. (2019). Fairness in Temporal Verification of Distributed Systems. In: Zamojski, W., Mazurkiewicz, J., Sugier, J., Walkowiak, T., Kacprzyk, J. (eds) Contemporary Complex Systems and Their Dependability. DepCoS-RELCOMEX 2018. Advances in Intelligent Systems and Computing, vol 761. Springer, Cham. https://doi.org/10.1007/978-3-319-91446-6_14

Download citation

Publish with us

Policies and ethics

Search

Navigation