Список потенциальных тем для научных работ

Верификация и анализ коммуникационных протоколов с помощью сетей Петри высокого уровня

Цель работы - применение современных методов и средств к анализу и верификации различных коммуникационных протоколов. Такие методы включают моделирование протоколов сетями Петри высокого уровня, анализ этих моделей с целью обнаружения ошибок и неэффективности реализации протоколов, а также метод проверки моделей для верификации сетей Петри. Особое внимание будет уделено анализу и верификации кольцевых протоколов.

Реализация контроля динамической семантики языка предикатного программирования P через систему автоматического доказательства mdl

Для предикатной программы во внутреннем представлении транслятора требуется сгенерировать на языке спецификаций системы mdl формулы корректности конструкций программы для последующего автоматического доказательства формул в системе mdl. Посылками формул являются предусловие и проходимые условия условных операторов.

В соответствии с семантикой языка P значение выражения должно принадлежать типу позиции, в которой находится выражение. Довольно часто тип определяется набором ограничений. Рассмотрим следующий фрагмент программы: