10.14489/vkit.2025.10.pp.003-009

DOI: 10.14489/vkit.2025.10.pp.003-009

Макаров К. С., Фаткин Р. И.
ДВУХЭТАПНЫЙ МЕТОД ОБНАРУЖЕНИЯ ДЕФЕКТОВ ПОЛЬЗОВАТЕЛЬСКОГО ИНТЕРФЕЙСА ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ НА ОСНОВЕ ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ И ВИЗУАЛЬНОГО ТЕСТИРОВАНИЯ
(с.3-9)

Аннотация. Обоснована необходимость объединения динамической верификации программного обеспечения (скриншотного тестирования) с формальными методами верификации. Предложен метод двухэтапной верификации, основанный на построении формальной модели интерфейса и интеграции ее с инструментами скриншотного тестирования. Методология включает построение иерархической автоматной модели интерфейса, формализацию UX-требований в темпоральных логиках и их проверку модель-чекером с итерационным уточнением CEGAR с последующей автоматической генерацией скриншотов ключевых состояний и сопоставлением с эталонами. Рассмотрены способы формализации требований к UX/UI, возможности применения методов проверки моделей (включая техники абстракции и CEGAR) для анализа интерфейса. Обозначены возможности и ограничения предложенного метода.

Ключевые слова: формальная верификация; модельная проверка; пользовательский интерфейс; визуальное регрессионное тестирование; иерархическая автоматная модель; требования UX; темпоральная логика LTL/CTL; автоматизация скриншотов; критически важные системы.

Makarov K. S., Fatkin R. I.
A TWO-STAGE METHOD FOR DETECTING SOFTWARE USER-INTERFACE DEFECTS BASED ON FORMAL VERIFICATION AND VISUAL TESTING
(pp.3-9)

Abstract. The article presents a two-stage method for detecting defects in software user interfaces that combines formal verification methods with automated screenshot testing. The approach is designed to address the limitations of traditional user interface testing by combining model checking with regression analysis based on screenshots. In the first step, a hierarchical model captures the state of the user interface, including transitions between screens, component visibility, and interaction logic. User interface requirements are formalized using temporal logics (LTL/CTL) and verified using model checking with CEGAR-based refinement when false counterexamples occur. In the second step, executable user interface scripts are generated using counterexamples and reproduced in browsers using automation tools. Interface states are captured as screenshots and compared to reference images to confirm or rule out visual inconsistencies. This hybrid method provides rigorous validation of critical UX properties and improves test reliability by reducing false positives. Key benefits include early detection of logical and visual problems, automation of scenario generation, and explicit indication of bugs in UX. Challenges include difficulties in maintaining up-to-date formal models and managing abstraction levels without loss of analytical rigor. The method is especially relevant for mission-critical applications, where UI behavior must be both correct and meet strict requirements.

Keywords: Formal verification; Model checking; User interface; Visual regression testing; Hierarchical automaton model; UX-requirements; Temporal logic LTL/CTL; Screenshot automation; Safety-critical systems.

+ - Информация об авторах (About the Authors) Click to collapse

Рус

К. С. Макаров, Р. И. Фаткин (Курский государственный университет, Курск, Россия) E-mail: Этот e-mail адрес защищен от спам-ботов, для его просмотра у Вас должен быть включен Javascript

Eng

K. S. Makarov, R. I. Fatkin (Kursk State University, Kursk, Russia) E-mail: Этот e-mail адрес защищен от спам-ботов, для его просмотра у Вас должен быть включен Javascript

+ - Библиографический список (References) Click to collapse

Рус

1. Campos J. C., Harrison M. D. Formal Approaches for Interactive Systems // Handbook of Human–Computer Interaction. 2025  [Электронный ресурс]. URL: https://link.springer.com/rwe/10.1007/978-3-319-27648-9_120-1  (дата обращения: 29.06.2025). DOI: 10.1007/978‑3‑319‑27648‑9_120‑1
2. Watson I., Reeves S., Masci P. Integrating User Design and Formal Models within PVSio‑Web [Электрон¬ный ресурс]. URL: https://arxiv.org/pdf/1811.10821 (дата обращения: 29.06.2025).
3. Pirelli S. V. Automated formal verification of software network functions : doctoral thesis. Lausanne : École Polytechnique Fédérale de Lausanne, 2024. 115 p.
4. Wang H. Temporal logic-based model checking for autonomous systems // International Journal of Engineering Inventions. 2024. V. 13, № 8. P. 82–90.
5. Dwyer M. B., Carr V., Hines L. Model checking graphical user interfaces using abstractions // Proceedings of the 6th European Software Engineering Conference combined with the 5th ACM SIGSOFT Symposium on Foundations of Software Engineering (ESEC/FSE ’97). Berlin : Springer, 1997. (Lecture Notes in Computer Science; Vol. 1301). P. 244–261. DOI: 10.1145/267895.267914
6. Campos J. C., Harrison M. D. From HCI to software engineering and back // Bridging the Gaps Between Software Engineering and Human–Computer Interaction: Proceedings of the ICSE’03 Workshop, Portland (OR, USA), 03 May 2003. New York : ACM, 2003. P. 49–56.
7. Hajdu A., Micskei Z. Efficient strategies for CEGAR-based model checking // Journal of Automated Reasoning. 2020. V. 64, № 1. P. 1051–1091. DOI: 10.1007/s10817-019-09535-x
8. Extraction and empirical evaluation of GUI-level invariants as GUI oracles in mobile app testing / A. A. Yarifard, S. Araban, S. Paydar, et al. // Information and Software Technology. 2025. [Электронный ресурс]. URL: https://pure.qub.ac.uk/files/611794631/PAPER_-_GUI_invariants.pdf (дата обращения: 21.03.2025). DOI: 10.1016/j.infsof.2024.107531
9. Campos J. C., Harrison M. D., Masci P., Curzon P. Verification of user-interface software: the example of use-related safety requirements and programmable medical devices // IEEE Transactions on Human-Machine Systems. 2017. V. 47, № 6. P. 834–846. [Электронный ресурс]. URL: https://webarchive.di.uminho.pt/haslab.uminho.pt/jccampos/files/medthmsv9-author_version.pdf (дата обращения: 28.03.2025). DOI: 10.1109/THMS.2017.2717910

Eng

1. Campos, J. C., & Harrison, M. D. (2025). Formal approaches for interactive systems. In Handbook of human–computer interaction. Springer. https://doi.org/10.1007/978-3-319-27648-9_120-1
2. Watson, I., Reeves, S., & Masci, P. (2018). Integrating user design and formal models within PVSio-web. arXiv. https://arxiv.org/pdf/1811.10821
3. Pirelli, S. V. (2024). Automated formal verification of software network functions [Doctoral dissertation, École Polytechnique Fédérale de Lausanne].
4. Wang, H. (2024). Temporal logic-based model checking for autonomous systems. International Journal of Engineering Inventions, 13(8), 82–90.
5. Dwyer, M. B., Carr, V., & Hines, L. (1997). Model checking graphical user interfaces using abstractions. In Proceedings of the 6th European Software Engineering Conference held jointly with the 5th ACM SIGSOFT Symposium on the Foundations of Software Engineering (pp. 244–261). Springer. https://doi.org/10.1145/267895.267914
6. Campos, J. C., & Harrison, M. D. (2003). From HCI to software engineering and back. In Bridging the gaps between software engineering and human–computer interaction: Proceedings of the ICSE'03 Workshop (pp. 49–56). Association for Computing Machinery.
7. Hajdu, A., & Micskei, Z. (2020). Efficient strategies for CEGAR-based model checking. Journal of Automated Reasoning, 64(1), 1051–1091. https://doi.org/10.1007/s10817-019-09535-x
8. Yarifard, A. A., Araban, S., Paydar, S., et al. (2025). Extraction and empirical evaluation of GUI-level invariants as GUI oracles in mobile app testing. Information and Software Technology. https://doi.org/10.1016/j.infsof.2024.107531
9. Campos, J. C., Harrison, M. D., Masci, P., & Curzon, P. (2017). Verification of user-interface software: The example of use-related safety requirements and programmable medical devices. IEEE Transactions on Human-Machine Systems, 47(6), 834–846. https://doi.org/10.1109/THMS.2017.2717910

+ - Заказать электронную версию статьи (Purchase digital version of a single article) Click to collapse

Рус

Статью можно приобрести в электронном виде (PDF формат).

Стоимость статьи 700 руб. (в том числе НДС 20%). После оформления заказа, в течение нескольких дней, на указанный вами e-mail придут счет и квитанция для оплаты в банке.

После поступления денег на счет издательства, вам будет выслан электронный вариант статьи.

Для заказа скопируйте doi статьи:

10.14489/vkit.2025.10.pp.003-009

и заполните форму

Отправляя форму вы даете согласие на обработку персональных данных.

Eng

This article is available in electronic format (PDF).

The cost of a single article is 700 rubles. (including VAT 20%). After you place an order within a few days, you will receive following documents to your specified e-mail: account on payment and receipt to pay in the bank.

After depositing your payment on our bank account we send you file of the article by e-mail.

To order articles please copy the article doi:

10.14489/vkit.2025.10.pp.003-009

and fill out the form