Специфікація та верифікація формальної моделі системи реального часу із використанням TLA+ - Шишацька, О. В.; Матійчук, Л. П.; Шишацький, А. В. (Центральноукраїнський науковий вісник. Технічні науки, 2025)
У роботі представлено розробку формальної моделі програмно-апаратної системи реального часу на прикладі системи безперервного моніторингу рівня глюкози (Continuous Glucose Monitoring, CGM). CGM-системи є критично важливими ІТ-рішеннями, що використовуються в медичному середовищі для постійного вимірювання рівня глюкози в крові та своєчасного сповіщення користувачів. З огляду на дедалі ширше впровадження CGM у замкнені контури керування (Closed-Loop Systems, CLS), які автоматизують введення інсуліну, зростає потреба у забезпеченні коректності таких систем, особливо враховуючи популярність неперевірених рішень, створених користувачами самостійно (DIY). Попри досягнення в галузі фізичних та сенсорних технологій, програмне забезпечення CGM-систем часто не має формальних специфікацій та перевірок. Це створює ризики у передбачуваності, безпеці та надійності, що є особливо критичними у медичних застосуваннях. Метою дослідження є застосування формальних методів, зокрема TLA+, для специфікації, моделювання та верифікації поведінки CGM-системи, що функціонує в режимі реального часу. Запропонована модель описує основні компоненти CGM-системи: цикли вимірювання в часі, збереження історичних даних, виявлення перевищень порогових значень і логіку сповіщення. Також модель фіксує інваріанти системи, зокрема правильну послідовність переходів між станами та своєчасне генерування сповіщень. Для реалізації обрано TLA+, що ґрунтується на темпоральній та модальній логіці, підтримує моделювання конкурентних та реактивних систем і має потужні інструменти, зокрема перевірку моделей TLC. Модель реалізовано та протестовано за допомогою TLA+ Toolbox і TLC. Розглянуто кілька конфігурацій (порогові значення глюкози, довжина історії, тривалість роботи системи) для оцінки її стійкості. Результати верифікації засвідчили відсутність тупикових станів і виконання всіх заданих властивостей безпеки. Це підтверджує доцільність використання формального моделювання в TLA+ для коректності CGM-систем, особливо в умовах, де критичними є безпечність, правильність та відслідковуваність. Модульна структура моделі забезпечує можливість її подальшого розширення — включення алгоритмів машинного навчання для прогнозування рівня глюкози, моделювання впливу фізичної активності або харчування, а також поступовий перехід до повністю автономних CLS-середовищ. Крім того, ця робота сприяє поширенню практик формальної специфікації в комп’ютерних науках, зокрема в галузі систем реального часу та критично важливих застосунків.