На сегодняшний день имеется очень много веб-приложений, которые содержат ошибку в логике работы. Большинство данных уязвимостей могут быть устранены при автоматизированном тестировании, кроме тех, что заключены в логике приложения.
Для выявления данных ошибок логики следует использовать формальные методы проверки. В данном случае в этой работе для проверки и выявление уязвимости в приложении был использован метод автоматической формальной верификации параллельных систем с конечным числом состояний. Для достижения этих задач была построена модель в утилите Spin, произведена верификация и получены результаты. Тем самым была произведена попытка демонстрации одной из уязвимостей в алгоритме веб – приложения.
Ключевые слова: верификация, проверка алгоритма, веб-приложение, безопасность приложения, логические ошибки, параллельные процессы, утилита Spin, model checking.
