Advertisement

Fairness in Distributed Systems Verification

  • Wiktor B. DaszczukEmail author
Chapter
Part of the Studies in Computational Intelligence book series (SCI, volume 817)

Abstract

Recall that in distributed systems three types of nondeterminism can be observed, modeled in IMDS.

References

  1. Baier, C., & Katoen, J.-P. (2008). Principles of model checking. Cambridge, MA: MIT Press. ISBN: 9780262026499.zbMATHGoogle Scholar
  2. Behrmann, G., David, A., & Larsen, K. G. (2006). A Tutorial on Uppaal 4.0. Aalborg, Denmark. url: http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf.
  3. Cimatti, A., Clarke, E., Giunchiglia, F., & Roveri, M. (2000). NUSMV: A new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2(4), 410–425.  https://doi.org/10.1007/s100090050046.
  4. Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model checking. Cambridge, MA: MIT Press.Google Scholar
  5. Daszczuk, W. B. (2001). Evaluation of temporal formulas based on “Checking By Spheres.” In Proceedings Euromicro Symposium on Digital Systems Design, Warsaw, Poland, 4–6 Sept. 2001 (pp. 158–164). IEEE.  https://doi.org/10.1109/dsd.2001.952267.
  6. Daszczuk, W. B. (2003). Verification of temporal properties in concurrent systems. Warsaw University of Technology. url: https://repo.pw.edu.pl/docstore/download/WEiTI-0b7425b5-2375-417b-b0fa-b1f61aed0623/Daszczuk.pdf.
  7. Dick, G., & Yao, X. (2014). Model representation and cooperative coevolution for finite-state machine evolution. In 2014 IEEE Congress on Evolutionary Computation (CEC), Beijing, China, 6–11 July 2014 (pp. 2700–2707). New York, NY: IEEE.  https://doi.org/10.1109/cec.2014.6900622.
  8. Gómez, R., & Bowman, H. (2005). Discrete Timed Automata. Technical Report 3-05-2005. Canterbury, UK. url: https://kar.kent.ac.uk/14362/1/TR305.pdf.
  9. Holzmann, G. J. (1995). Tutorial: Proving properties of concurrent systems with SPIN. In 6th International Conference on Concurrency Theory, CONCUR’95, Philadelphia, PA, 21–24 Aug 1995 (pp. 453–455). Berlin Heidelberg: Springer-Verlag.  https://doi.org/10.1007/3-540-60218-6_34.
  10. Holzmann, G. J. (1997). The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), 279–295.  https://doi.org/10.1109/32.588521.CrossRefGoogle Scholar
  11. Hung, Y. -C., & Chen, G. -H. (2006). Reverse reachability analysis: A new technique for deadlock detection on communicating finite state machines. Software: Practice and Experience, 23(9), 965–979.  https://doi.org/10.1002/spe.4380230904.
  12. Katoen, J.-P. (1999). Concepts, algorithms, and tools for model checking. Germany: Erlangen-Nürnberg. url: http://www.cs.aau.dk/~kgl/VERIFICATION99/katoen2.psGoogle Scholar
  13. Kesten, Y., Pnueli, A., & Raviv, L. (1998). Algorithmic verification of linear temporal logic specifications. In 25th International Colloquium, ICALP’98 Aalborg, Denmark, 13–17 July 1998 (pp. 1–16). Berlin Heidelberg: Springer-Verlag.  https://doi.org/10.1007/bfb0055036.
  14. Laskowski, E., Tudruj, M., Olejnik, R., & Toursel, B. (2005). Java byte code scheduling based on the most-often-used-paths in programs with branches. In The 4th International Symposium on Parallel and Distributed Computing (ISPDC’05), Lille, France, 4–6 July 2005 (pp. 21–27). New York, NY: IEEE.  https://doi.org/10.1109/ispdc.2005.31.
  15. Pnueli, A., & Sa’ar, Y. (2008). All you need is compassion. In 9th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2008, San Francisco, CA, 7–9 Jan. 2008 (pp. 233–247). Berlin Heidelberg: Springer-Verlag.  https://doi.org/10.1007/978-3-540-78163-9_21.
  16. Rozier, K. Y. (2011). Linear temporal logic symbolic model checking. Computer Science Review, 5(2), 163–203.  https://doi.org/10.1016/j.cosrev.2010.06.002.CrossRefzbMATHGoogle Scholar
  17. Scholten, C. S., & Dijkstra, E.W. (1982). A class of simple communication patterns. In Selected Writings on Computing: A personal Perspective (pp. 334–337). New York, NY: Springer.  https://doi.org/10.1007/978-1-4612-5695-3_60.
  18. Zerzelidis, A., & Wellings, A. J. (2005). Requirements for a real-time .NET framework. ACM SIGPLAN Notices, 40(2), 41.  https://doi.org/10.1145/1052659.1052666.

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Institute of Computer ScienceWarsaw University of TechnologyWarsawPoland

Personalised recommendations