DOI: https://doi.org/10.32515/2664-262X.2025.11(42).2.38-44
Специфікація та верифікація формальної моделі системи реального часу із використанням TLA+
Про авторів
Шишацька Олена Володимирівна , кандидат фізико-математичних наук, доцент кафедри теорії та технології програмування факультету комп’ютерних наук та кібернетики, Київський національний університет імені Тараса Шевченка, м. Київ, Україна, https://orcid.org/0000-0001-8791-8989, e-mail: shyshatska@knu.ua
Матійчук Любомир Павлович, доцент, доктор економічних наук, професор кафедри комп’ютерних наук, Тернопільський національний технічний університет імені Івана Пулюя, ORCID: https://orcid.org/0000-0001-6701-4683, e-mail: mlpstat@gmail.com.
Шишацький Андрій Вікторович, асистент кафедри теорії та технології програмування факультету комп’ютерних наук та кібернетики, Київський національний університет імені Тараса Шевченка, м. Київ, Україна, https://orcid.org/0009-0000-5038-1110, e-mail: ashyshatskyy@knu.ua
Анотація
У роботі представлено розробку формальної моделі програмно-апаратної системи реального часу на прикладі системи безперервного моніторингу рівня глюкози (Continuous Glucose Monitoring, CGM). CGM-системи є критично важливими ІТ-рішеннями, що використовуються в медичному середовищі для постійного вимірювання рівня глюкози в крові та своєчасного сповіщення користувачів. З огляду на дедалі ширше впровадження CGM у замкнені контури керування (Closed-Loop Systems, CLS), які автоматизують введення інсуліну, зростає потреба у забезпеченні коректності таких систем, особливо враховуючи популярність неперевірених рішень, створених користувачами самостійно (DIY). Попри досягнення в галузі фізичних та сенсорних технологій, програмне забезпечення CGM-систем часто не має формальних специфікацій та перевірок. Це створює ризики у передбачуваності, безпеці та надійності, що є особливо критичними у медичних застосуваннях. Метою дослідження є застосування формальних методів, зокрема TLA+, для специфікації, моделювання та верифікації поведінки CGM-системи, що функціонує в режимі реального часу.
Запропонована модель описує основні компоненти CGM-системи: цикли вимірювання в часі, збереження історичних даних, виявлення перевищень порогових значень і логіку сповіщення. Також модель фіксує інваріанти системи, зокрема правильну послідовність переходів між станами та своєчасне генерування сповіщень. Для реалізації обрано TLA+, що ґрунтується на темпоральній та модальній логіці, підтримує моделювання конкурентних та реактивних систем і має потужні інструменти, зокрема перевірку моделей TLC. Модель реалізовано та протестовано за допомогою TLA+ Toolbox і TLC. Розглянуто кілька конфігурацій (порогові значення глюкози, довжина історії, тривалість роботи системи) для оцінки її стійкості. Результати верифікації засвідчили відсутність тупикових станів і виконання всіх заданих властивостей безпеки. Це підтверджує доцільність використання формального моделювання в TLA+ для коректності CGM-систем, особливо в умовах, де критичними є безпечність, правильність та відслідковуваність. Модульна структура моделі забезпечує можливість її подальшого розширення — включення алгоритмів машинного навчання для прогнозування рівня глюкози, моделювання впливу фізичної активності або харчування, а також поступовий перехід до повністю автономних CLS-середовищ. Крім того, ця робота сприяє поширенню практик формальної специфікації в комп’ютерних науках, зокрема в галузі систем реального часу та критично важливих застосунків.
Ключові слова
системи реального часу, CGM, модель, формальні методи проєктування, специфікація, TLA+, верифікація
Повний текст:
PDF
Посилання
1. Rafeh, R., & Rabiee, A. (2013). Towards the design of safety-critical software. Journal of Applied Research and Technology, 11, 683–694.
2. Capozucca, A., & Guelfi, N. (2006). The fault-tolerant insulin pump. In Rigorous Development of Complex Fault-Tolerant Systems (pp. 59–75). Berlin: Springer-Verlag.
3. Lamport, L. (2002). Specifying systems: The TLA+ language and tools for hardware and software engineers. Boston: Addison-Wesley Professional.
4. Wayne, H. (2018). Practical TLA+: Planning driven development. New York: Apress.
5. Fainekos, G., Kress-Gazit, H., & Pappas, G. (2005). Temporal logic motion planning for mobile robots. In Proceedings of the 2005 IEEE International Conference on Robotics and Automation (pp. 2020–2025). Barcelona: IEEE.
6. Humberstone, L. (2016). Philosophical applications of modal logic. London: College Publications.
7. Kripke, S. (1962). Semantical considerations for modal logics. Acta Philosophica Fennica, Helsinki, 389.
8. Guéron, J. (2008). Time and modality (Studies in Natural Language and Linguistic Theory; Vol. 75). Dordrecht: Springer.
9. Newcombe, C., Rath, T., Zhang, F., et al. (2015). How Amazon Web Services uses formal methods. Communications of the ACM, 58(4), 66–73.
10. Henzinger, T.A., & Sifakis, J. (2006). The discipline of embedded systems design. IEEE Computer, 39(10), 36–44.
11. Woodcock, J., Larsen, P.G., Bicarregui, J., & Fitzgerald, J. (2009). Formal methods: Practice and experience. ACM Computing Surveys (CSUR), 41(4), Article 19, 1–3.
12. AndrewShysh. (2025, February 15). Blood glucose monitoring model: Specification and verification [GitHub repository]. GitHub. https://github.com/AndrewShysh/TLAPLUS_CGM_System/tree/main.
Пристатейна бібліографія
1. Rafeh, R., Rabiee, A. Towards the design of safety-critical software. Journal of Applied Research and Technology. 2013. Vol. 11. P. 683–694.
2. Capozucca, A., Guelfi, N. The fault-tolerant insulin pump. Rigorous Development of Complex Fault-Tolerant Systems. Berlin : Springer-Verlag, 2006. P. 59–75.
3. Lamport, L. Specifying systems: The TLA+ language and tools for hardware and software engineers. Boston : Addison-Wesley Professional, 2002. 384 p.
4. Wayne, H. Practical TLA+: Planning driven development. New York : Apress, 2018. 221 p.
5. Fainekos, G., Kress-Gazit, H., Pappas, G. Temporal logic motion planning for mobile robots. Proceedings of the 2005 IEEE International Conference on Robotics and Automation. Barcelona, 2005. P. 2020–2025.
6. Humberstone, L. Philosophical applications of modal logic. London : College Publications, 2016. 588 p.
7. Kripke, S. Semantical considerations for modal logics. Acta Philosophica Fennica. 1962. Helsinki. 389 p.
8. Guéron, J. Time and modality. (Studies in Natural Language and Linguistic Theory ; Vol. 75). Dordrecht : Springer, 2008. 316 p.
9. Newcombe, C., Rath, T., Zhang, F. et al. How Amazon Web Services uses formal methods. Communications of the ACM. 2015. Vol. 58, No. 4. P. 66–73.
10. Henzinger, T. A., Sifakis, J. The discipline of embedded systems design. IEEE Computer. 2006. Vol. 39, No. 10. P. 36–44.
11. Woodcock, J., Larsen, P. G., Bicarregui, J., Fitzgerald, J. Formal methods: Practice and experience. ACM Computing Surveys (CSUR). 2009. Vol. 41, No. 4. Article No. 19. P. 1–3.
12. Blood glucose monitoring model: specification and verification. Github: веб-сайт. URL: https://github.com/AndrewShysh/TLAPLUS_CGM_System/tree/main (дата звернення: 15.02.2025).
Copyright (c) 2025 О. В. Шишацька, Л. П. Матійчук, А. В. Шишацький
Специфікація та верифікація формальної моделі системи реального часу із використанням TLA+
Про авторів
Шишацька Олена Володимирівна , кандидат фізико-математичних наук, доцент кафедри теорії та технології програмування факультету комп’ютерних наук та кібернетики, Київський національний університет імені Тараса Шевченка, м. Київ, Україна, https://orcid.org/0000-0001-8791-8989, e-mail: shyshatska@knu.ua
Матійчук Любомир Павлович, доцент, доктор економічних наук, професор кафедри комп’ютерних наук, Тернопільський національний технічний університет імені Івана Пулюя, ORCID: https://orcid.org/0000-0001-6701-4683, e-mail: mlpstat@gmail.com.
Шишацький Андрій Вікторович, асистент кафедри теорії та технології програмування факультету комп’ютерних наук та кібернетики, Київський національний університет імені Тараса Шевченка, м. Київ, Україна, https://orcid.org/0009-0000-5038-1110, e-mail: ashyshatskyy@knu.ua
Анотація
Ключові слова
Повний текст:
PDFПосилання
1. Rafeh, R., & Rabiee, A. (2013). Towards the design of safety-critical software. Journal of Applied Research and Technology, 11, 683–694.
2. Capozucca, A., & Guelfi, N. (2006). The fault-tolerant insulin pump. In Rigorous Development of Complex Fault-Tolerant Systems (pp. 59–75). Berlin: Springer-Verlag.
3. Lamport, L. (2002). Specifying systems: The TLA+ language and tools for hardware and software engineers. Boston: Addison-Wesley Professional.
4. Wayne, H. (2018). Practical TLA+: Planning driven development. New York: Apress.
5. Fainekos, G., Kress-Gazit, H., & Pappas, G. (2005). Temporal logic motion planning for mobile robots. In Proceedings of the 2005 IEEE International Conference on Robotics and Automation (pp. 2020–2025). Barcelona: IEEE.
6. Humberstone, L. (2016). Philosophical applications of modal logic. London: College Publications.
7. Kripke, S. (1962). Semantical considerations for modal logics. Acta Philosophica Fennica, Helsinki, 389.
8. Guéron, J. (2008). Time and modality (Studies in Natural Language and Linguistic Theory; Vol. 75). Dordrecht: Springer.
9. Newcombe, C., Rath, T., Zhang, F., et al. (2015). How Amazon Web Services uses formal methods. Communications of the ACM, 58(4), 66–73.
10. Henzinger, T.A., & Sifakis, J. (2006). The discipline of embedded systems design. IEEE Computer, 39(10), 36–44.
11. Woodcock, J., Larsen, P.G., Bicarregui, J., & Fitzgerald, J. (2009). Formal methods: Practice and experience. ACM Computing Surveys (CSUR), 41(4), Article 19, 1–3.
12. AndrewShysh. (2025, February 15). Blood glucose monitoring model: Specification and verification [GitHub repository]. GitHub. https://github.com/AndrewShysh/TLAPLUS_CGM_System/tree/main.
Пристатейна бібліографія
1. Rafeh, R., Rabiee, A. Towards the design of safety-critical software. Journal of Applied Research and Technology. 2013. Vol. 11. P. 683–694.
2. Capozucca, A., Guelfi, N. The fault-tolerant insulin pump. Rigorous Development of Complex Fault-Tolerant Systems. Berlin : Springer-Verlag, 2006. P. 59–75.
3. Lamport, L. Specifying systems: The TLA+ language and tools for hardware and software engineers. Boston : Addison-Wesley Professional, 2002. 384 p.
4. Wayne, H. Practical TLA+: Planning driven development. New York : Apress, 2018. 221 p.
5. Fainekos, G., Kress-Gazit, H., Pappas, G. Temporal logic motion planning for mobile robots. Proceedings of the 2005 IEEE International Conference on Robotics and Automation. Barcelona, 2005. P. 2020–2025.
6. Humberstone, L. Philosophical applications of modal logic. London : College Publications, 2016. 588 p.
7. Kripke, S. Semantical considerations for modal logics. Acta Philosophica Fennica. 1962. Helsinki. 389 p.
8. Guéron, J. Time and modality. (Studies in Natural Language and Linguistic Theory ; Vol. 75). Dordrecht : Springer, 2008. 316 p.
9. Newcombe, C., Rath, T., Zhang, F. et al. How Amazon Web Services uses formal methods. Communications of the ACM. 2015. Vol. 58, No. 4. P. 66–73.
10. Henzinger, T. A., Sifakis, J. The discipline of embedded systems design. IEEE Computer. 2006. Vol. 39, No. 10. P. 36–44.
11. Woodcock, J., Larsen, P. G., Bicarregui, J., Fitzgerald, J. Formal methods: Practice and experience. ACM Computing Surveys (CSUR). 2009. Vol. 41, No. 4. Article No. 19. P. 1–3.
12. Blood glucose monitoring model: specification and verification. Github: веб-сайт. URL: https://github.com/AndrewShysh/TLAPLUS_CGM_System/tree/main (дата звернення: 15.02.2025).
Copyright (c) 2025 О. В. Шишацька, Л. П. Матійчук, А. В. Шишацький