Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 13

Communication Papers of the 2017 Federated Conference on Computer Science and Information Systems

Threefold Analysis of Distributed Systems: IMDS, Petri Net and Distributed Automata DA3

DOI: http://dx.doi.org/10.15439/2017F32

Citation: Communication Papers of the 2017 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 13, pages 377–386 ()

Full text

Abstract. Integrated Model of Distributed Systems is used to model and verify distributed systems. In the formalism, a system is modeled as a set of servers' states and agents' messages. The operation of a system is modeled as actions converting global system configuration (a set of states and messages) to a new configuration. The formalism is used in Dedan verification environment, in which specification and verification of distributed systems is performed. For the graphical specification and simulation of distributed systems, Distributed Autonomous and Asynchronous Automata (DA3) are invented. Such simulation does not require calculation of global configuration space of a system. Two forms of DA3 are shown: Server-DA3 (SDA3) for the server view and Agent-DA3 (ADA3) for the agent view.

References

  1. S. Chrobot and W. B. Daszczuk, “Communication Dualism in Distributed Systems with Petri Net Interpretation,” Theor. Appl. Informatics, vol. 18, no. 4, pp. 261–278, 2006. https://taai.iitis.pl/taai/article/view/250/taai-vol.18-no.4-pp.261
  2. W. B. Daszczuk, “Communication and Resource Deadlock Analysis using IMDS Formalism and Model Checking,” Comput. J., vol. 60, no.2, pp.729–750 (2017). http://dx.doi.org/10.1093/comjnl/bxw099
  3. C. A. R. Hoare, “Communicating sequential processes,” Commun. ACM, vol. 21, no. 8, pp. 666–677, Aug. 1978. http://dx.doi.org/10.1145/359576.359585
  4. R. Milner, A Calculus of Communicating Systems. Berlin Heidelberg: Springer-Verlag, 1984. ISBN: 0387102353
  5. E. M. Clarke, O. Grumberg, and D. Peled, Model Checking. Cambridge, MA: MIT Press, 1999. ISBN: 0-262-03270-8
  6. “Dedan” http://staff.ii.pw.edu.pl/dedan/files/DedAn.zip
  7. W. B. Daszczuk and W. M. Zuberek, “Deadlock detection in distributed systems using the IMDS formalism and Petri nets,” in 12th International Conference on Dependability and Complex Systems, DepCoS-RELCOMEX 2017, Brunów, Poland, 2-6 July 2017, Advances in Intelligent Systems and Computing, vol 582, pp.118-130, Springer, Cham, 2018. http://dx.doi.org/10.1007/978-3-319-59415-6_12
  8. D. C. Craig and W. M. Zuberek, “Two-stage siphon-based deadlock detection in Petri nets,” in Current Advances in Computing, Engineering and Information Technology, P. Petratos and P. Dandapami, Eds. Palermo, Italy: Int. Society for Advanced Research, 2008, pp. 317–330.
  9. W. Zielonka, “Notes on finite asynchronous automata,” RAIRO - Theor. Informatics Appl. - Inform. Théorique Appl., vol. 21, no. 2, pp. 99–135, 1987. http://archive.numdam.org/ARCHIVE/ITA/ITA_1987__21_2/ITA_1987__21_2_99_0/ITA_1987__21_2_99_0.pdf
  10. P. Krishnan, “Distributed Timed Automata,” Electron. Notes Theor. Comput. Sci., vol. 28, pp. 5–21, 2000. doi 10.1016/S1571-0661(05)80627-9
  11. D. Van Chieu and D. Van Hung, “An Extension of Mazukiewicz Traces and their Applications in Specification of Real-Time Systems,” in 2010 Second International Conference on Knowledge and Systems Engineering, Hanoi, Vietnam, October 7-9, 2010, 2010, pp. 167–171. http://dx.doi.org/10.1109/KSE.2010.39
  12. V. Diekert and A. Muscholl, “On Distributed Monitoring of Asynchronous Systems,” in 19th International Workshop on Logic, Language, Information and Computation, WoLLIC 2012, Buenos Aires, Argentina, September 3-6, 2012, 2012, pp. 70–84. http://dx.doi.org/10.1007/978-3-642-32621-9_5
  13. M. Mukund, “Automata on Distributed Alphabets,” in Modern Applications of Automata Theory, Co-Published with Indian Institute of Science (IISc), Bangalore, India, 2012, pp. 257–288. http://dx.doi.org/10.1142/9789814271059_0009
  14. L. Brim, I. Černá, P. Moravec, and J. Šimša, “How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors,” Electron. Notes Theor. Comput. Sci., vol. 135, no. 2, pp. 3–18, Feb. 2006. http://dx.doi.org/10.1016/j.entcs.2005.10.015
  15. B. Bollig and M. Leucker, “A Hierarchy of Implementable MSC Languages,” in Formal Techniques for Networked and Distributed Systems - FORTE 2005, Taipei, Taiwan, October 2-5, 2005, 2005, pp. 53–67. http://dx.doi.org/10.1007/11562436_6
  16. M. S. Balan, “Serializing the Parallelism in Parallel Communicating Pushdown Automata Systems,” Electron. Proc. Theor. Comput. Sci., vol. 3, pp. 59–68, Jul. 2009. http://dx.doi.org/10.4204/EPTCS.3.5
  17. G. Behrmann, A. David, and K. G. Larsen, “A Tutorial on Uppaal 4.0,” Report, Univ. Aalborg, Denmark, 2006. http://www.uppaal.com/admin/anvandarfiler/filer/uppaal-tutorial.pdf
  18. M. Heiner, M. Schwarick, and J.-T. Wegener, “Charlie – An Extensible Petri Net Analysis Tool,” in 36th International Conference, PETRI NETS 2015, Brussels, Belgium, June 21-26, 2015, 2015, pp. 200–211. http://dx.doi.org/10.1007/978-3-319-19488-2_10
  19. Charlie, “Charlie Petri net analyzer.” . http://www-dssz.informatik.tu-cottbus.de/DSSZ/Software/Charlie
  20. M. Schwarick, M. Heiner, and C. Rohr, “MARCIE - Model Checking and Reachability Analysis Done EffiCIEntly,” in 2011 Eighth International Conference on Quantitative Evaluation of SysTems, Aachen, Germany, 5-8 Sept. 2011, 2011, pp. 91–100. http://dx.doi.org/10.1109/QEST.2011.19
  21. K. Jensen and L. M. Kristensen, Coloured Petri Nets. Berlin, Heidelberg: Springer-Verlag, 2009. http://dx.doi.org/10.1007/b95112
  22. “UML” http://www.uml.org/.
  23. G. Dick and X. Yao, “Model representation and cooperative coevolution for finite-state machine evolution,” in 2014 IEEE Congress on Evolutionary Computation (CEC), Beijing, China, 6-11 July 2014, 2014, pp. 2700–2707. http://dx.doi.org/10.1109/CEC.2014.6900622
  24. W. B. Daszczuk, “Evaluation of temporal formulas based on ‘checking by spheres’” in Proceedings Euromicro Symposium on Digital Systems Design, Warsaw, Poland, 4-6 September 2001, 2001, pp. 158–164. http://dx.doi.org/10.1109/DSD.2001.952267
  25. B. Czejdo, S. Bhattacharya, M. Baszun, and W. B. Daszczuk, “Improving Resilience of Autonomous Moving Platforms by real-time analysis of their Cooperation,” Autobusy-TEST, vol. 17, no. 6, pp. 1294–1301, 2016. http://www.autobusy-test.com.pl/images/stories/Do_pobrania/2016/nr%206/logistyka/10_l_czejdo_bhattacharya_baszun_daszczuk.pdf
  26. Z. Garofalaki, D. Kallergis, G. Katsikogiannis, I. Ellinas, and C. Douligeris, “Transport services within the IoT ecosystem using localisation parameters,” in 2016 IEEE International Symposium on Signal Processing and Information Technology (ISSPIT), Limassol, Cyprus, 12-14 December 2016, 2016, pp. 87–92. http://dx.doi.org/10.1109/ISSPIT.2016.7886014
  27. W. B. Daszczuk, M. Bielecki, and J. Michalski, “Rybu: Imperative-style Preprocessor for Verification of Distributed Systems in the Dedan Environment,” in KKIO’17 – Software Engineering Conference, Rzeszów, Poland, 14-16 Sept 2017, 2017, accetped.
  28. C. Lewerentz and T. Lindner, Eds., Formal Development of Reactive Systems, LNCS 891. Berlin, Heidelberg: Springer-Verlag, 1995. http://dx.doi.org/10.1007/3-540-58867-1
  29. W. B. Daszczuk, “Asynchronous Specification of Production Cell Benchmark in Integrated Model of Distributed Systems,” in 23rd International Symposium on Methodologies for Intelligent Systems, ISMIS 2017, Warsaw, Poland, 26-29 June 2017, 2017.
  30. “Dedan Examples” http://staff.ii.pw.edu.pl/dedan/files/examples.zip
  31. A. Derezińska, R. Pilitowski, Correctness issues of UML class and state machine models in the C# code generation and execution framework, in: M. Ganzha, M. Paprzycki, T. Pełech-Pilichowski Eds., 2008 Int. Multiconference Comput. Sci. Inf. Technol. Wisła, Poland, 20-22 Oct. 2008, IEEE, Piscataway, NJ, 2008: pp. 517–524. http://dx.doi.org/10.1109/IMCSIT.2008.4747293