Аннотация:В данной работе рассматривается задача верификации реализации сетевого протокола для сетевого процессорного устройства (СПУ). Современные сетевые протоколы сложны и имеют множество состояний. Поэтому важно проводить комплексную проверку реализации сетевого протокола на соответствие спецификации.
Формальная верификация является одним из этапов проверки реализации сетевого протокола на соответствие его спецификации. Данный этап позволяет доказать выполнение формальных требований предъявляемых к реализации сетевого протокола. Использование автоматических средств верификации позволяет ускорить процесс верификации. Такие средства используют специальные языки описания моделей, поэтому требуется алгоритмы трансляции модели реализации в описание модели на языке средства автоматической верификации.
Также для проведения автоматической формальной верификации необходимо проводить сокращение формальной модели реализации сетевого протокола, так как большинство методов автоматической верификации имеют проблемы с большими моделями и экспоненциальным ростом проверяемых состояний. Поэтому возникает задача построить отношение абстракции, в котором будут отсекаться особенности архитектуры не влияющие на верификацию реализации сетевого протокола.