Abstract
Recall that in distributed systems three types of nondeterminism can be observed, modeled in IMDS.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Baier, C., & Katoen, J.-P. (2008). Principles of model checking. Cambridge, MA: MIT Press. ISBN: 9780262026499.
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.
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.
Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model checking. Cambridge, MA: MIT Press.
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.
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.
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.
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.
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.
Holzmann, G. J. (1997). The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), 279–295. https://doi.org/10.1109/32.588521.
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.
Katoen, J.-P. (1999). Concepts, algorithms, and tools for model checking. Germany: Erlangen-Nürnberg. url: http://www.cs.aau.dk/~kgl/VERIFICATION99/katoen2.ps
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.
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.
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.
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.
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.
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.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Daszczuk, W.B. (2020). Fairness in Distributed Systems Verification. In: Integrated Model of Distributed Systems. Studies in Computational Intelligence, vol 817. Springer, Cham. https://doi.org/10.1007/978-3-030-12835-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-12835-7_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-12834-0
Online ISBN: 978-3-030-12835-7
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)