Интеллектуалды жүйелерді әзірлеу және тармақталған бисимуляциялық модельдеу арқылы ықтималдық синхрондалған автоматтармен әуе қозғалысын басқарушы-ұшқыш интерфейсін формальды талдау

Жоба жетекшісі: Shazada Muhammad Umair Khan, PhD Интеллектуалды жүйелер және киберқауіпсіздік  департаментінің қауымдастырылған профессоры

Жобаның мақсаты: Бұл жобаның мақсаты ықтималдық уақытша автоматтан (PTA) интерфейсті құру және салалық бисимуляциялық талдау арқылы ресми тексеруді жүзеге асыру болып табылады. Негізгі мақсат – ықтималдық белгісіздік пен нақты уақыттағы қатаң шектеулер жағдайында оператор мен автоматтандырылған жүйе арасында болжамды және қауіпсіз өзара әрекеттесуді орнату.

1. Зерттеу мақсатты жүйенің сыртқы бақылаудан немесе енуден қорғайтын анықтамалық жүйемен бірдей әрекет ететінін растау үшін мінез-құлық эквиваленттілігін талдау арқылы жүйе қасиеттерін тексереді.
2. Зерттеу жүйелі және тиімді әзірлеу әдістерін орнату үшін пайдаланушы интерфейсін жобалаудың негізгі әрекеттерін анықтайды.
3. Зерттеу пайдаланушылардың өзара әрекеттесуінің бірнеше тәсілдерін бағалайды, олардың айрықша ерекшеліктері мен практикалық қолданылуын, сондай-ақ олардың ыңғайлылыққа әсерін зерттейді.
4. Зерттеу қатеге бейім күйлерді жою арқылы қадағалаушы басқару интерфейстерін және пайдаланушы интерфейсінің беріктігін жақсартуға арналған дизайн принциптерін әзірлейді.
5. Зерттеу жарияланады.

Бұл жұмыс пайдаланушы интерфейсі мен жүйе әрекетіне назар аудара отырып, бағдарламалық қамтамасыз ету жүйесінің сенімділігін, ыңғайлылығын және қауіпсіздігін жақсарту мақсаттарын белгілейді. Бірінші мақсат құпиялылықты сақтай отырып, жүйелерді сыртқы бақылаудан қорғау үшін мінез-құлық эквиваленттілігін пайдаланып сипаттарды ресми түрде тексеруді қамтиды. Екінші және үшінші мақсаттар пайдаланушы тәжірибесін жақсарту үшін негізгі дизайн әрекеттерін анықтау және бірнеше өзара әрекеттесу мәнерлерін бағалау арқылы пайдаланушы интерфейсінің дизайны мен өзара әрекеттесу аспектілеріне назар аударады. Соңғы мақсат пайдаланушы интерфейстеріндегі жүйелік қателер мен сәтсіздіктерді бақылауға және алдын алуға мүмкіндік беретін күшті дизайн принциптерін әзірлеуге бағытталған. Бұл мақсаттар қауіпсіз, пайдаланушыға бағытталған және сәтсіздікке төзімді бағдарламалық жасақтама жүйелерін жасау үшін бірге жұмыс істейді.

1. Талаптарды ресімдеу кезеңінде алынған барлық контроллер-ұшқыш, авионика және бақылаушы бақылау өзара әрекеттесуі ықтималдық уақыты бар автоматты дәл модельдейтін 358-күй Марков шешім қабылдау процесіне (MDP) түрлендірілді. Ғаламдық таймер t нақты уақыт мерзімдерін көрсету үшін бір белгі бір жарым секундқа тең болатын жиырма белгі циклін пайдаланды (1-суретті қараңыз).

2. Композиттік MDP кең ауқымды іздеуден өтті, 23 итерацияда жинақталып, 946 ықтималдық ауысулары анықталды. Беллман теңдеулері қол жетімділік пен күтілетін сыйақы мәселелеріне арналған мән итерациясы арқылы шешілді, қалдық қате {10}^{-6}-тан төмен төмендеді, бұл пессимистік және оптимистік жоспарлау стратегияларының сандық дұрыстығын растайды.

3. Барлығы он алты PTCTL қасиеті бағаланды. Кез келген жоспарлау стратегиясы, мейлі дұшпандық немесе кооперативтік болсын, миссияның сөзсіз аяқталуына әкеледі, өйткені аяқтау белгісінің сөзсіз қол жетімділігі дәлелдеді.

Ең нашар жағдайдағы қате:

қате іске қосулардың 10%-да орын алғанын білдіреді.

Ең жақсы жағдай:

Белгілі бір жоспарлау стратегияларымен экипаж ауытқуларды толығымен болдырмайтынын көрсетеді.

4.  r_2 Марапаттау құрылымы миссияны аяқтамас бұрын күтілетін қателер санын есептеді.

Ең жақсы стратегия:

Ең нашар стратегия:

бұл жоспарлаудың сенімділікке әсерін көрсетеді.

5. r_1 сыйақы құрылымы аяқтау уақытын кенелермен өлшейді.

Ең аз мән:

Максималды мән:

ол шектеулі орындау уақыты терезесін көрсетеді.

6. 10-белгіленген қызмет мақсаты шектеулі уақытқа қол жеткізуге әкелді:

Ішкі растаудың кешігуіне байланысты маршруттардың 4,95%-ы ғана уақытында аяқталды.

7.  Қауіпсіздік инварианты:

миссия аяқталғаннан кейін қателердің болмауын қамтамасыз етті.

Бисимуляция инварианты:

модельдеу барысында байқалған интерфейс пен авионикалық модель арасындағы сәйкестікті қамтамасыз етті.

8. Қадағалаудың вето механизмі дұрыс жұмыс істеді, себебі:

барлық ықтимал дұшпандық стратегиялар бойынша.

9. Косараджу алгоритмін қолданып графикті декомпозициялау бір-бірімен тығыз байланысты үш құрамдас бөлікті анықтады: күту, растау және орындау. Жылу картасындағы диагональды жолақпен (2-сурет) және Санкей диаграммасындағы кең жолақпен (3-сурет) көрінетіндей, растау компоненті шамамен 70% стационарлық ықтималдық үлестіріміне ие болды.

10. Барлық ықтималдық пен сыйақы көрсеткіштері 4-суреттегі бағаналы диаграммада графикалық түрде салыстырылады, бұл миссияның аяқталу ықтималдығының қатаң шектерін және қателер мен уақыттың елеулі өзгерістерін көрсетеді.

Толық сандық пакет 2-суреттің жанында берілген 1-кестеде жинақталған.

Сурет 1. Жүйенің модульдік құрылымы синхрондау нүктелерімен (16 күй) жүйенің негізін құрайды. Жүйе төрт тарату әрекеті арқылы байланысатын тоғыз PRISM модулін қамтиды: енгізу, кері байланыс, u_done және force_done және жаһандық таймер t. Фрухтерман-Рейнгольд позициялау әдісі визуалды орналасудың әрбір шетіне күйдің өту ықтималдығын орналастырады.

Сурет 2. Өтпелі тығыздықтың жылу картасы.  матрицасы үш жұмыс істейтін СКҚ-ны (күту, растау, жіберу) диагональ бойынша орындалатын тізбекті блоктарға ұйымдастырады. Пиксель қарқындылығы өту ықтималдығын көрсетеді; растау SCC стационарлық ықтималдық массасының ~70% қамтитын ең жарқын блок ретінде пайда болады.

Сурет 3. Ықтималдық ағынының Сэнкей диаграммасы. Бұл диаграммадағы түйіндердің өлшемдері үш СКҚ стационарлық күйінің және аяқталу күйінің ықтималдығын көрсетеді. Растау SCC диаграммадағы таспаның қалыңдығымен көрсетілгендей жіберу және аяқтау күйлеріне ағынның ең үлкен мөлшерін шығарады.

4-суреттегі бағаналы диаграмма ықтималдық пен сыйақы көрсеткіштерін көрсетеді. Тікелей салыстыруды жеңілдету үшін барлық сегіз метрика максималды мәндеріне дейін қалыпқа келтіріледі: аяқтау ықтималдығы бірлікте қалады, қателер мен кідіріс күтулері кеңірек диапазонды көрсетеді және уақытқа байланысты қол жеткізу мерзімінің қысымы кезінде өнімділікті баса көрсетеді.

Shazada Muhammad Umair Khan

Жоба жетекшісі, PhD, Есептреулер және деректре туралы ғылым  департаментінің қауымдастырылған профессоры

Хасен Акбота

Жобаның орындаушысы, Astana IT University 3 курс студенті

Мырзабек Камила

Жобаның орындаушысы, Astana IT University 3 курс студенті