Разработан метод верификации корректности RPC-протоколов с использованием фреймворка LTest. Метод учитывает недетерминированность сетевых задержек и отказов, проверяя все возможные исполнения исходного кода. Для этого исполнение моделируется в однопоточной среде с виртуальными потоками, управляемыми планировщиком. Были протестированы реализации протоколов на основе UDP и TCP, доработана поддержка динамического числа потоков. Оптимизирован перебор состояний системы за счёт эквивалентных исполнений. В результате фреймворк LTest адаптирован для тестирования RPC, что повысило уверенность в его корректности.

Черкашин Н.К. (науч. рук. Аксенов В.Е.) Разработка методов верификации корректности rpc протокола // Сборник тезисов докладов конгресса молодых ученых. Электронное издание. – СПб: Университет ИТМО, [2025]. URL: https://kmu.itmo.ru/digests/article/14085