УАҚЫТТЫҚ ЫҚТИМАЛДЫ АВТОМАТТАР НЕГІЗІНДЕ ӘУЕ ҚОЗҒАЛЫСЫН БАСҚАРУ ЖҮЙЕЛЕРІН ТАЛДАУ К.К.
##plugins.pubIds.doi.readerDisplayName##:
https://doi.org/10.54309/IJICT.2025.23.3.014Кілт сөздер:
probabilistic, timed automata, human-machine interaction, interface verification, air traffic control, bisimulationАңдатпа
Бұл зерттеу жобасы әуе қозғалысын басқарудың интеллектуалды жүйесін әзірлеуді ұшқыштар мен диспетчерлер арасындағы басқару әрекеттерін үйлестіру интерфейстерін қатаң математикалық бағалаумен біріктіреді. «Диспетчер–ұшқыш» интерфейсі бірыңғай реактивті жүйені бейнелейтіндіктен, ол ұшу басқару бағдарламалық жасақтамасы сияқты формалды спецификацияларға ие болуы тиіс. Жүйенің әрбір өзара әрекеттесуі нақты уақыттағы операциялық шектеулерді және адам қателері мен жабдықтың істен шығуының кездейсоқ туындауын бейнелейтін уақыттық ықтималды автоматпен модельденеді. Z формалды спецификация тілі адамның да, машинаның да тексере алатын шарттар мен салдарларға байланысты бақыланатын сыртқы әрекеттерді сипаттауға мүмкіндік береді. Операторларды, графикалық дисплейлерді, ішкі авиониканы және қадағалау қауіпсіздік агенттерін бейнелейтін интерфейс модульдері уақыттық белгісіздік жағдайында мінез-құлық эквиваленттілігін дәлелдейтін әлсіз тармақталатын бисимуляцияны орындау үшін біріктіріледі.
Модель диспетчер командаларының, машинаның кері байланысының, қадағалау вето шешімдерінің және ұшқыш растауларының барлық маңызды уақыттық және істен шығу сценарийлерін қамтитын жиырма жаһандық күйде көрсетілуі мүмкін екенін дәлелдейді. Автоматтандырылған верификация жүйесі миссияның сәтті аяқталу ықтималдығының төмендігін, жалпы тәуекелді арттыратын оператор қателерін тіркейді және жасырын жобалау осалдықтарын анықтайтын уақыттық дивергенттік орындау жолдарын айқындайды. Интерфейс инженерлері уақыттық шарттарды өзгерте алады, визуалды белгілерді қайта қарай алады және когнитивтік жүктемеге бейімделулерді енгізе алады, өйткені графикалық дисплей мен жасырын логиканың эквиваленттігі ресми түрде дәлелденген. Бұл зерттеу «диспетчер–ұшқыш» интерфейсін математикалық сертификаттауға ие болатын әуе қозғалысын басқару экожүйесінің құрамдас бөлігіне айналдырады және жұмыс жүктемесі деректеріне бейімделетін болашақ интерфейстердің негізін қалайды, сонымен қатар машиналар тексере алатын қауіпсіздік кепілдіктерін қамтамасыз етеді.
##plugins.generic.usageStats.downloads##
Жүктеулер
Жарияланды
Дәйексөзді қалай келтіруге болады
Журналдың саны
Бөлім
Лицензия
Авторлық құқық (c) 2025 ХАЛЫҚАPАЛЫҚ АҚПАРАТТЫҚ ЖӘНЕ КОММУНИКАЦИЯЛЫҚ ТЕХНОЛОГИЯЛАР ЖУРНАЛЫ
Бұл жұмыс Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 Дүние жүзінде.
https://creativecommons.org/licenses/by-nc-nd/3.0/deed.en