Голева М.А.
ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ ЛОГИЧЕСКИХ РАССУЖДЕНИЙ В ЗАДАЧАХ БИЗНЕС-ПРОЦЕССОВ НА ПРИМЕРЕ ПРОДАЖИ ЖЕЛЕЗНОДОРОЖНЫХ БИЛЕТОВ *
Аннотация:
в работе рассматривается применение аппарата логики высказываний для формальной верификации корректности рассуждений, описывающих бизнес-процесс продажи железнодорожных билетов.
Ключевые слова:
логика высказываний, формальная верификация, бизнес-процесс, тавтология, логический вывод, железнодорожные билеты, информационные системы
В современных интеллектуальных информационных системах, автоматизирующих сложные бизнес-процессы, ключевое значение имеет корректность и непротиворечивость заложенных в них правил. Одним из эффективных инструментов для проверки такой корректности является формальная логика, в частности, логика высказываний. Она позволяет трансформировать словесные описания процессов в строгие логические формулы и анализировать их на предмет наличия логических следствий и противоречий. Формальная верификация в контексте программных и информационных систем — это процесс математически обоснованного доказательства соответствия системы её формальной спецификации. Формальная верификация стремится доказать корректность системы для всех возможных сценариев её работы. Для этого необходимо построение формальной модели системы и логический или алгоритмический анализ этой модели на предмет выполнения заданных свойств (корректности, безопасности, живучести)[2]. Синтаксис логики высказываний определяет правила построения корректных формул из пропозициональных переменных и логических связок (¬, ∧, ∨, →, ↔)[1]. Семантика задаёт значение формулы через истинностные значения её переменных, что отражается в таблицах истинности. А тавтология (формула, истинная при всех наборах значений) и логическое следствие (ситуация, когда истинность посылок гарантирует истинность заключения) составляют основу проверки корректности рассуждений [2]. Целью данной работы является демонстрация методики применения логики высказываний для верификации цепочки рассуждений в рамках типичного бизнес-процесса – продажи железнодорожного билета. Рассмотрим процесс продажи железнодорожного билета. Известны следующие утверждения: Пассажир может купить билет только если есть свободные места и он предоставил корректные данные. Если пассажир хочет купить билет и параметры рейса введены, то система проверяет наличие мест. Система оформляет билет тогда и только тогда, когда оплата прошла успешно и место забронировано. Если нет свободных мест, то процесс завершается, или пассажиру предлагается альтернативный рейс. Пассажир подтверждает выбор места и оплачивает билет, либо он отказывается от покупки. Если данные пассажира некорректны или оплата не прошла, то билет не оформляется. Место бронируется только если пассажир подтвердил выбор и система сгенерировала счет. Система сгенерирует счет если и только если место забронировано и выбран способ оплаты. Требуется проверить логическую правильность рассуждения: Если пассажир хочет купить билет и ввел параметры рейса, то система проверит наличие мест. Если есть свободные места и пассажир предоставил корректные данные, то место будет забронировано. Если место забронировано и пассажир подтвердил выбор, то система сгенерирует счет. Если счет сгенерирован и оплата прошла успешно, то билет будет оформлен. Следовательно, если пассажир хочет купить билет, ввел параметры рейса, предоставил корректные данные, подтвердил выбор и оплата прошла успешно, то билет будет оформлен. Далее введём логические переменные и запишем посылки в виде формул. Полученное выражение тождественно равно 1, следовательно, формула является тавтологией, и рассуждения логически правильны. Также используем метод построения таблицы истинности. У нас 10 переменных (A, B, C, D, E, F, G, H, I, J), поэтому полная таблица будет иметь 210=1024210=1024 строк. Вместо этого я построю сокращённую таблицу для ключевых случаев, где S (конъюнкция посылок) истинно, и проверю, всегда ли при этом Z истинно. Таблица 1. Таблица истинности. Для всех наборов переменных, где S=1, Z=1.Формула S→Z — тавтология. Значит рассуждение логически правильно. В ходе исследования была успешно применена методология логики высказываний для формальной верификации корректности рассуждения в рамках заданного бизнес-процесса. Корректность вывода, связывающего начальные действия пассажира (желание купить билет, ввод данных, подтверждение, успешную оплату) с конечным результатом (оформление билета), была строго доказана двумя независимыми методами: аналитическим (преобразования и доказательство от противного) и табличным (сокращённая таблица истинности). Для полной верификации динамики бизнес-процессов необходимо привлечение более мощного аппарата — темпоральных логик, логики предикатов.
Номер журнала Вестник науки №12 (93) том 4 ч. 1
Ссылка для цитирования:
Голева М.А. ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ ЛОГИЧЕСКИХ РАССУЖДЕНИЙ В ЗАДАЧАХ БИЗНЕС-ПРОЦЕССОВ НА ПРИМЕРЕ ПРОДАЖИ ЖЕЛЕЗНОДОРОЖНЫХ БИЛЕТОВ // Вестник науки №12 (93) том 4 ч. 1. С. 709 - 715. 2025 г. ISSN 2712-8849 // Электронный ресурс: https://www.вестник-науки.рф/article/27853 (дата обращения: 07.02.2026 г.)
Вестник науки © 2025. 16+