Threefold analysis of distributed systems: IMDS, Petri net and distributed automata DA3

• Autorzy: Daszczuk Wiktor

Identyfikatory

DOI

10.15439/2017F32

• Konferencja: Communication Papers of the 2017 Federated Conference on Computer Science and Information Systems
• Języki publikacji: EN

Abstrakty

EN

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.

• Wydawca: Polskie Towarzystwo Informatyczne
• Czasopismo: Annals of Computer Science and Information Systems
• Rocznik: 2017
• Tom: Vol. 13
• Strony: 377--386
• Opis fizyczny: Bibliogr. 31 poz., rys., tab.

Twórcy

autor

Daszczuk Wiktor

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

Bibliografia

• 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