Improving resilience of autonomous moving platforms by real-time analysis of their cooperation

• Autorzy: Czejdo B. , Bhattacharya S. , Baszun M. , Daszczuk W. B.

Warianty tytułu

PL

Poprawa bezpieczeństwa autonomicznych platform mobilnych drogą analizy ich współpracy w czasie rzeczywistym

• Języki publikacji: EN

Abstrakty

EN

Environmental changes, failures, collisions or even terrorist attacks can cause serious malfunctions of the delivery systems. We have presented a novel approach improving resilience of Autonomous Moving Platforms AMPs. The approach is based on multi-level state diagrams describing environmental trigger specifications, movement actions and synchronization primitives. The upper level diagrams allowed us to model advanced interactions between autonomous AMPs and detect irregularities such as deadlocks live-locks etc. The techniques were presented to verify and analyze combined AMPs’ behaviors using model checking technique. The described system, Dedan verifier, is still under development. In the near future, a graphical form of verified system representation is planned.

PL

Zmiany w otoczeniu, awarie, kolizje czy nawet ataki terrorystyczne mogą spowodować poważne awarie w systemach transportowych. W artykule zaprezentowaliśmy nowe podejście do poprawy odporności autonomicznych platform mobilnych (AMPs). Podejście to opiera się na specyfikacji przy pomocy wielopoziomowych diagramach stanów, opisujących wpływ otoczenia, podejmowane akcje komunikacyjne i prymitywy synchronizacyjne. Schematy na górnym poziomie pozwoliły modelować zaawansowane interakcje między autonomicznymi pojazdami i wykrywać nieprawidłowości, takie jak zakleszczenia, częściowe zakleszczenia itp. Zaprezentowano techniki zastosowane w celu weryfikacji i analizy łącznego zachowania pojazdów techniką weryfikacji modelowej. Opisany system weryfikacyjny Dedan jest wciąż w fazie rozwoju. W niedalekiej przyszłości planowana jest graficzna forma reprezentacji weryfikowanego systemu.

Słowa kluczowe

EN

Autonomous Moving Platforms; safety; Dedan verifier system

PL

platforma mobilna autonomiczna; bezpieczeństwo; system weryfikacyjny Dedan

• Wydawca: Instytut Naukowo-Wydawniczy "SPATIUM". sp. z o.o.
• Czasopismo: Autobusy : technika, eksploatacja, systemy transportowe
• Rocznik: 2016
• Tom: R. 17, nr 6
• Strony: 1294--1301
• Opis fizyczny: Bibliogr. 28 poz. rys.., pełen tekst na CD

Twórcy

autor

Czejdo B.

• Department of Mathematics and Computer Science, Fayetteville State University, Fayetteville, NC 28301, USA

autor

Bhattacharya S.

• Department of Mathematics and Computer Science, Fayetteville State University, Fayetteville, NC 28301, USA

autor

Baszun M.

• Warsaw University of Technology, Depart-ment of Electronics and Information Technology

autor

Daszczuk W. B.

• Warsaw University of Technology, Department of Electronics and Information Technology

Bibliografia

• 1. Irving J. Fundamentals of Personal Rapid Transit. Lexington, MA: Lexington Books, 1978, ISBN is 0-669-02520-8.
• 2. Johnson RE, Walter HT, Wild WA. Analysis and Simulation of Automated Vehicle Stations. In: Gary DA, Girrard WL, Kornhauser AL (eds.). Personal Rapid Transit III. Minneapolis: University of Minnesota, 1976, 269–281.
• 3. Choromański W, Daszczuk W, Grabski W, Dyduch J, Maciejewski M, Brach P. Personal Rapid Transit (PRT) Computer Network Simulation and Analysis of Flow Capacity. Automated People Movers and Transit Systems 2013. Reston, VA: American Society of Civil Engineers, 2013, 296–312.
• 4. Visser J, Konings R, Wiegmans BW, Pielage B-JA. A New Hinterland Transport Concept for the Port of Rotterdam: Organisational and/or Technological Challenges? Transportation Research Forum, 48th Annual Forum, Boston University. Fargo, ND: Transportation Research Forum, 2007.
• 5. Murphy R. Introduction to AI Robotics. MIT Press, 2000, ISBN 0-262-13383-0.
• 6. Desouza GN, Kak AC. Vision for mobile robot navigation: a survey. IEEE Trans Pattern Anal Mach Intell 2002;24:237–267.
• 7. Blank D. Robots make computer science personal. Commun ACM 2006;49:25-27, DOI: 10.1145/1183236.1183254.
• 8. Kumar D. Learning Computing with AMPs (Python). Institute for Personal AMPs in Education, 2007.
• 9. Meng Y. Multi-Robot Searching using Game-Theory Based Approach. Int J Adv Robot Syst 2008;5:341–350.
• 10. Harel D. On visual formalisms. Commun ACM 1988;31:514–530, DOI: 10.1145/42411.42414.
• 11. Rumbaugh J, Blaha M, Premerlani W, Eddy F, Lorensen W. Object-Oriented Modeling and Design. New Jersey, NJ: Prentice Hall, 1990, ISBN 0-13-629841-9.
• 12. Czejdo BD, Bhattacharya S. Programming Robots with State Diagrams. J Comput Sci Coll 2009;24:19–26.
• 13. Bhattacharya S, Czejdo BD, Mobley S. An Integrated Computer Vision and Infrared Sensor Based Approach to Autonomous Robot Navigation in an Indoor Environment. 7th International Conference on Computing, Communications and Control Technologies. 2009, 42–47.
• 14. Galamhos C, Matas J, Kittler J. Progressive probabilistic Hough transform for line detection. Proceedings. 1999 IEEE Computer Society Conference on Computer Vision and Pattern Recognition (Cat. No PR00149). New York, NY: IEEE Comput. Soc, 1999, 554–560, DOI: 10.1109/CVPR.1999. 786993.
• 15. Czejdo B, Bhattacharya S, Czejdo J. Use of Probabilistic State Diagrams for Robot Navigation in an Indoor Environment. Proceedings of the Annual International Conference on Advances in Distributed and Parallel Computing ADPC 2010 ADPC 2010. Global Science and Technology Forum, 2010, A97–A102, DOI: 10.5176/978-981-08-7656-2ATAI2010-63.
• 16. McMillan KL. Symbolic Model Checking. Norwell, MA: Kluwer Academic Publishers, 1993, ISBN 0792393805.
• 17. Berard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, P. S. Systems and Software Verification. Model-Checking Techniques and Tools. Berlin Heidelberg: Springer-Verlag, 2001, ISBN 978-3-662-04558-9.
• 18. Holzmann GJ. The model checker SPIN. IEEE Trans Softw Eng 1997;23:279–295, DOI: 10.1109/32.588521.
• 19. Peled DA. Software Reliability Methods. Berlin Heidelberg: Springer, 2001, ISBN 978-1-4419-2876-4.
• 20. Clarke EM, Wing JM. Formal methods: state of the art and future directions. ACM Comput Surv 1996;28:626–643.
• 21. Bryant RE. Binary decision diagrams and beyond: enabling technologies for formal verification. Proceedings of IEEE International Conference on Computer Aided Design (ICCAD). New York, NY: IEEE Comput. Soc. Press, 1995, 236–243, DOI: 10.1109/ICCAD.1995.480018.
• 22. Daszczuk WB. Verification of Temporal Properties in Concurrent Systems. PhD Thesis, Warsaw University of Technology, Institute of Computer Science, 2003, DOI: 10.13140/RG.2.1.2779.6565.
• 23. Chrobot S, Daszczuk WB. Communication Dualism in Distributed Systems with Petri Net Interpretation. Theor Appl Informatics 2006;4:261–278.
• 24. Daszczuk WB. Deadlock and Termination Detection Using IMDS Formalism and Model Checking, Version 2, ICS WUT Technical Report No.2/2008. Warsaw, Poland, 2008.
• 25. Jia W, Zhou W. Distributed Network Systems. From Concepts to Implementations. New York: Springer, 2005, ISBN 0-387-23839-5.
• 26. Alur R, Dill DL. A theory of timed automata. Theor Comput Sci 1994;126:183–235, DOI: 10.1016/0304-3975(94)90010-8.
• 27. Daszczuk WB. Real Time Model Checking Using Timed Concurrent State Machines. Int J Comput Sci Appl 2006;4:1–12.
• 28. Kwiatkowska M, Norman G, Parker D. PRISM 4.0: Verification of Probabilistic Real-Time Systems. 2011, 585–591, DOI: 10.1007/978-3-642-22110-1_47.

Uwagi

EN

This research was supported by the Belk Foundation in the case of Bogdan Czejdo and Sambit Bhattacharya.