|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ИНХС РАН |
||
Метод абстракции чередований потоков для верификации моделей многопоточных программкурсовая работа (Специалист)
- Научный руководитель: Миронов А.М.
- Автор: Руденчик Вероника Павловна
- Тип: Специалист
- Организация, в которой проходила защита: МГУ имени М.В. Ломоносова
- Кафедра: Кафедра математической теории интеллектуальных систем
- Год защиты: 2022
- Курс: 4
- Аннотация: Данная работа посвящена проблеме верификации многопоточных программ. Из существующих методов верификации многопоточных программ анализ с раздельным рассмотрением потоков показал свою эффективность. Данный анализ работает достаточно быстро, но может пропускать ошибки. В связи с этим актуальной задачей является увеличение точности этого анализа без значительной потери его эффективности. На практике это может быть сделано с использованием теории CPA (англ. Configurable Program Analysis), которая позволяет единым образом описывать различные техники анализа и комбинировать их. Целью данной работы была разработка и реализация метода абстракции чередования потоков на основе анализа с раздельным рассмотрением потоков. В работе описана теория CPA и анализ с раздельным рассмотрением потоков в терминах теории CPA. Предложен метод абстракции чередования потоков, основной идеей которого является отслеживание порядка выполнения операторов в каждом потоке. Метод описан в терминах теории CPA и реализован в инструменте верификации CPAchecker. Представлена конфигурация инструмента верификации, использующая предложенный метод абстракции чередования потоков на основе анализа с раздельным рассмотрением потоков. Полученные результаты показывают, что метод позволяет повысить точность анализа с раздельным рассмотрением потоков для некоторых классов задач.
- Добавил в систему: Миронов Андрей Михайлович