Közúti fedezőjelzőrendszer formális modellezése UPPAAL keretrendszer felhasználásával
Formal modelling of level crossing system for trams using UPPAAL framework
Keywords:
urban railway, modelling, functionality, formal methods, timed automataAbstract
Development based on systems modelling is a widely used technique in the engineering practice. Formal modelling and verification is an effective set of tools that combines modelling with mathematical precision. In this paper, we present the formal modelling of an urban railway safety-critical system using the UPPAAL framework.
Kivonat
A rendszerek modellezésén alapuló fejlesztés széles körben használt technika a mérnöki gyakorlatban. A formális modellezés és verifikáció egy hatékony eszközkészlet, amely a modellezést kombinálja a matematikai precizitással. E cikkben egy városi vasúti biztonságkritikus rendszer formális modellezését mutatjuk be az UPPAAL keretrendszer felhasználásával.
References
A. Kunnappilly, P. Backeman, C. Seceleanu, From UML Modeling to UPPAAL Model checking of 5G Dynamic Service Orchestration, ECBS 2021, Conference on the Engineering of Computer Based Systems, doi: 10.1145/3459960.3459965.
Unified Modeling Language (OMG UML), 2017, Version 2.5.1.
F. Vaandrager, A First Introduction to Uppaal, 2011
D. Darvas Practice-Oriented Formal Methods to Support the Software Development of Industrial Con-trol Systems, 2016, doi: 10.5281/zenodo.162950.
Yul Y. Nazaruddin, Tua A. Tamba, K. Pradityo, B. Aristyo, A. Widyotriatmo, Safety Verification of a Train Interlocking Timed Automaton Model, IFAC-PapersOnLine, Volume 52, Issue 15, 2019, Pages 331-335, ISSN 2405-8963, https://doi.org/10.1016/j.ifacol.2019.11.696.
Wang Keming, Wang Zheng, Zhang Chuandong, Formal Modeling and Data Validation of General Railway Interlocking System, 16th Internal Conference on Railway Engineering Design & Operation, Lisbon, Portugal, 2018, vol. 181, pp. 527-538, ISSN 1743-3509, doi: https://doi.org/10.2495/CR180471.
CENELEC EN 50126:2017 Railway applications – The Specification and Demonstration of Reliability, Availability, Maintainability and Safety (RAMS) – Part 1: Generic RAMS Process (English version).
A. van Lamsweerde Requirements Engineering: From System Goals to UML Models to Software Speci-fications, 2009, ISBN: 978-0-470-01270-3.
H. Colin Requirements Management, The Interface Between Requirements Development and All Other Systems Engineering Processes, 2007, Springer-Verlag Berlin and Heidelberg GmBH & Co. KG, ISBN: 9783540476894.
IBM Rational DOORS, Requirements Management Framework Add-On, User Manual, Release 6.1, 2013
D. Long, Z. Scott A primer for Model-Based Systems Engineering (2nd edition), 2011, ISBN 978-1-105-58810-5.
H. Heinrich Model-Driven Development of Advanced User Interfaces, 2011, ISBN13: 9783642145612.
B. R. Hunt, R. L. Lipsman, J. m. Rosenberg, et al. A guide to MATLAB for Beginners and Experienced Users, Cambridge University, 2001, ISBN-13: 978-0-511-07792-0.
Devendra K. Chaturvedi, Modeling and Simulation of Systems Using MATLAB and Simulink, 2010, ISBN 9781439806722.
J. Holt, S. Perry SysML for Model-Based Systems Engineering, Institution of Engineering and Technol-ogy, 2013, ISBN: 1849196516.
CENELEC EN 50128:2011 Railway applications – Communication, signaling and processing systems – Software for railway control and protection systems (English version).
Jiacun Wang, William Tepfenhart, Formal Methods in Computer Science, 2019, ISBN 9781498775328
Barry Boehm, Dan Port & A. Winsor Brown (2002) Balancing Plan-Driven and Agile Methods in Soft-ware Engineering Project Courses, Computer Science Education, 12:3, 187-195, doi: 10.1076/csed.12.3.187.8617.
PO Asagba, EE Ogheneovo, A Comparative Analysis of Structured and Obejct-Oriented Programming methods, African Journals (AJOL), vol. 11. No. 4 (2007), doi: 10.4314/jasem.v11i4.55190.
Campean F., Henshall E., Yildirim U., Uddin A., Williams H. (2013) A Structured Approach for Func-tion Based Decomposition of Complex Multi-disciplinary Systems. In: Abramovici M., Stark R. (eds) Smart Product Engineering. Lecture Notes in Production Engineering. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30817-8_12.
Herrigel S, Laumanns M, Nash A, Weidmann U. Hierarchical Decomposition Methods for Periodic Railway Timetabling Problems. Transportation Research Record. 2013;2374(1):73-82. doi:10.3141/2374-09.
Budapest Transport Privately Held Corporation (BKV), Requirements booklet for safety elements and equipment for traffic control of trams (BKV-VILL-1.04), 2011.
1/1975. (II.5.) KPM-BM együttes rendelet a közúti közlekedés szabályiról.
