10.14489/vkit.2026.07.pp.003-007

DOI: 10.14489/vkit.2026.07.pp.003-007

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

Аннотация. Представлены операционализация и экспериментальная проверка интегрированного двухэтапного метода верификации пользовательских интерфейсов (UI) веб-приложений. Метод F = F2 × G × F1 объединяет CTL-верификацию конечно-автоматной модели (этап F1), оператор согласования G, транслирующий контрпримерные трассы в исполняемые Selenium-сценарии, и попиксельное сравнение снимков экрана с эталоном (этап F2). Состояния UI операционализируются тройкой наблюдаемых браузерных атрибутов, события – параметризованными действиями WebDriver. Введены метрики межуровневой согласованности Cons и ConfRate. Эксперимент на демонстрационном веб-приложении (пять контролируемых дефектов) показал, что интегрированный метод обнаруживает четыре дефекта против трех у формального и двух у динамического подхода; ConfRate = 1,0 подтверждает отсутствие ложных срабатываний оракула на формально корректных состояниях; значение Cons = 0,583 отражает долю состояний с согласованным вердиктом на обоих уровнях.

Ключевые слова: верификация пользовательского интерфейса; CTL-верификация; Selenium WebDriver; визуальная проверка; CEGAR; метрики межуровневой согласованности.

Fatkin R. I.
INTEGRATED TWO-STAGE METHOD FOR WEB APPLICATION USER INTERFACE VERIFICATION: OPERATIONALIZATION, CONSISTENCY METRICS, AND EXPERIMENTAL EVALUATION
(pp. 3-7)

Abstract. Verifying web application user interfaces demands simultaneous coverage of behavioural invariants, permissible interaction sequences, and visual fidelity. No single existing technique satisfies all three: CTL model checking delivers specification coverage but lacks pixel-level access; visual regression testing detects layout anomalies yet misses logical defects; functional testing provides no state-space coverage guarantees. This paper operationalizes and experimentally evaluates an integrated two-stage verification method. UI states are formalized as triples of observable browser attributes – DOM snapshots, computed CSS properties, and geometric layout data – enabling automatic predicate labelling without manual annotation. A reconciliation operator translates counterexample traces into executable Selenium scenarios and attaches pixel-level oracle structures. Two cross-level consistency metrics are introduced: Ccons, measuring verdict agreement across both stages, and Coracle, confirming absence of false activations on formally correct states. Evaluation used a Flask-based demo store with 11 states, 13 events, and 5 injected defects across four classes. The integrated method detected 4 defects versus 3 for the formal-only and 2 for the dynamic-only approach. One duplicate-order violation – encoded as AG(order_duplicate) – remained beyond reach of dynamic testing since both confirmation screens are visually identical. Coracle equalled 1.0, confirming zero false positives. Limitations include insensitivity of pixel comparison to opacity-hidden elements and manual model construction.

Keywords: User interface verification; CTL model checking; Selenium WebDriver; Visual testing; CEGAR; Cross-level consistency metrics.

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

Рус

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

Eng

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

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

Рус

1. Clarke E.M., Emerson E.A. Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic // Logic of Programs: Workshop. LNCS 131. Berlin: Springer, 1982. P. 52–71.
2. Clarke E.M., Grumberg O., Peled D. Model Checking. Cambridge: MIT Press, 1999. 314 p.
3. Фаткин Р.И. Скриншотное тестирование как многоаспектный вид автоматизированной динамической верификации веб-приложений // Программные системы и вычислительные методы. 2025. № 1. С. 32–54. DOI: 10.7256/2454-0714.2025.1.73535
4. Myers G.J., Sandler C., Badgett T. The Art of Software Testing. 3rd ed. Hoboken: John Wiley & Sons, 2011. 240 p.
5. The Oracle Problem in Software Testing: A Survey / Barr E.T., Harman M., McMinn P. et al. // IEEE Transactions on Software Engineering. 2015. V. 41, No. 5. P. 507–525.
6. Макаров К.С., Фаткин Р.И. Двухэтапный метод обнаружения дефектов пользовательского интерфейса программного обеспечения на основе формальной верификации и визуального тестирования // Вестник компьютерных и информационных технологий. 2025. Т. 22, № 10. С. 3–9. DOI: 10.14489/vkit.2025.10.pp.003-009
7. Counterexample-Guided Abstraction Refine-ment / E.M. Clarke, O. Grumberg, S. Jha et al. // Proceedings of 12th International Conference (CAV 2000). 15–19 Jul 2000. Chicago. Illinois. LNCS, V. 1855. Berlin: Springer, 2000. P. 154–169.
8. Wang Z., Bovik A.C., Sheikh H.R., Simoncelli E.P. Image Quality Assessment: From Error Visibility to Structural Similarity // IEEE Transactions on Image Processing. 2004. V. 13, No. 4. P. 600–612.

Eng

1. Clarke, E. M., & Emerson, E. A. (1982). Design and synthesis of synchronization skeletons using branching time temporal logic. In Logic of Programs: Workshop (LNCS 131, pp. 52–71). Springer.
2. Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model checking. MIT Press.
3. Fatkin, R. I. (2025). Screenshot testing as a multi aspect type of automated dynamic verification of web applications. Programmnye sistemy i vychislitel'nye metody, (1), 32–54. [in Russian language]. https://doi.org/10.7256/2454-0714.2025.1.73535
4. Myers, G. J., Sandler, C., & Badgett, T. (2011). The art of software testing (3rd ed.). John Wiley & Sons.
5. Barr, E. T., Harman, M., McMinn, P., et al. (2015). The oracle problem in software testing: A survey. IEEE Transactions on Software Engineering, 41(5), 507–525.
6. Makarov, K. S., & Fatkin, R. I. (2025). A two stage method for detecting software user interface defects based on formal verification and visual testing. Vestnik komp'yuternykh i informatsionnykh tekhnologiy, 22(10), 3–9. [in Russian language]. https://doi.org/10.14489/vkit.2025.10.pp.003-009
7. Clarke, E. M., Grumberg, O., Jha, S., et al. (2000). Counterexample guided abstraction refinement. In Proceedings of 12th International Conference on Computer Aided Verification (CAV 2000) (LNCS 1855, pp. 154–169). Springer.
8. Wang, Z., Bovik, A. C., Sheikh, H. R., & Simoncelli, E. P. (2004). Image quality assessment: From error visibility to structural similarity. IEEE Transactions on Image Processing, 13(4), 600–612.

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

Рус

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

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

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

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

10.14489/vkit.2026.07.pp.003-007

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

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

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.2026.07.pp.003-007

and fill out the form