Narzędzia help

Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
first previous next last
cannonical link button

http://yadda.icm.edu.pl:80/baztech/element/bwmeta1.element.baztech-6ab8a90d-13a7-429b-9ecd-33cce2801f6f

Czasopismo

Autobusy : technika, eksploatacja, systemy transportowe

Tytuł artykułu

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

Autorzy Czejdo, B.  Bhattacharya, S.  Baszun, M.  Daszczuk, W. B. 
Treść / Zawartość
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
PL autonomiczne platformy mobilne   bezpieczeństwo   system weryfikacyjny Dedan  
EN Autonomous Moving Platforms   safety   Dedan verifier system  
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, bczejdo@uncfsu.edu
autor Bhattacharya, S.
  • Department of Mathematics and Computer Science, Fayetteville State University, Fayetteville, NC 28301, USA, sbhattac@uncfsu.edu
autor Baszun, M.
autor Daszczuk, W. B.
  • Warsaw University of Technology, Department of Electronics and Information Technology, wbd@ii.pw.edu.pl
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.
Kolekcja BazTech
Identyfikator YADDA bwmeta1.element.baztech-6ab8a90d-13a7-429b-9ecd-33cce2801f6f
Identyfikatory