Для студентов СПбГУ по предмету Любой или несколько предметовНаправляемое свойством символьное исполнение программ на платформе .NETНаправляемое свойством символьное исполнение программ на платформе .NET
4,9551034
2024-07-172024-07-17СтудИзба
Курсовая работа: Направляемое свойством символьное исполнение программ на платформе .NET
Описание
Оглавление
3
4
Введение
Задача проверки качества и надежности кода является очень акту-альной. При этом программное обеспечение может быть существенно разным с точки зрения требований качества: во-первых, критически важные медицинское и военное ПО, ошибки в которых могут влиять на жизни людей; во-вторых, прикладное и промышленное ПО, и це-на ошибок в этих приложениях может стоить существенных денежных потерь, и, наконец, любительские приложения, ошибки которых влия-ют на настроение пользователей. Отметим, что количество критически важного ПО нарастает и, по факту, требования к нему увеличивают-ся. Одной из методик проверки качества и надежности кода является символьное исполнение [3].
Комбинаторный взрыв множества путей исполнения является также помехой для обратного символьного исполнения [7], которое начинается из заданной точки программы и двигается в сторону начальной точки входа в программу. Обратное символьное исполнение необходимо, на-пример, для генерации полного тестового покрытия веток программы. Отчасти справится с проблемой роста множества состояний помога-ет использование различных стратегий исследования кода. Стратегия исследования — это функция, котор
| Введение | 5 | ||
| 1. Обзор | 8 | ||
| 1.1. | Символьноеисполнение ................... | 8 | |
| 1.1.1. | Ограничения символьного исполнения . . . . . . . | 9 | |
| 1.1.2. | Стратегия исследования . . . . . . . . . . . . . . . | 9 | |
| 1.2. | Композициональное символьное исполнение . . . . . . . . | 10 | |
| 1.3. | Обратное символьное исполнение . . . . . . . . . . . . . . | 11 | |
| 1.4. | Формальная верификация программ . . . . . . . . . . . . | 12 | |
- Алгоритм символьного исполнения, направляемого свой-
| ством | 14 | ||
| 2.1. | Основныепонятия....................... | 14 | |
| 2.2. | Идеяалгоритма........................ | 15 | |
| 2.3. | Стратегияисследования . . . . . . . . . . . . . . . . . . . | 17 | |
| 2.4. | Типы данных, глобальные переменные . . . . . . . . . . . | 18 | |
| 2.5. | Алгоритм............................ | 20 | |
| 2.5.1. | Основныепроцедуры ................ | 21 | |
| 2.5.2. | Вспомогательные процедуры и функции . . . . . . | 28 | |
| 2.6. | Пример............................. | 30 | |
| 2.6.1. | Подготовительная работа . . . . . . . . . . . . . . | 31 | |
| 2.6.2. | Трассировка...................... | 33 | |
| 3. Реализация на платформе .NET | 37 | ||
| 3.1. | СистемаV# .......................... | 37 | |
| 3.2. | Cхема работы направляемой тестовой подсистемы . . . . | 38 | |
| 3.3. | Реализация стратегий исследований кода . . . . . . . . . | 39 | |
| 3.3.1. | DFS-иBFS-стратегии . . . . . . . . . . . . . . . . | 39 | |
| 3.3.2. | Направленная стратегия . . . . . . . . . . . . . . . | 40 | |
| 4. Эксперименты | 42 |
| 4.1. Проектирование эксперимента . . . . . . . . . . . . . . . . | 42 |
3
| 4.2. Результаты экспериментов . . . . . . . . . . . . . . . . . . | 44 |
| 5. Заключение | 45 |
| Список литературы | 46 |
4
Введение
Задача проверки качества и надежности кода является очень акту-альной. При этом программное обеспечение может быть существенно разным с точки зрения требований качества: во-первых, критически важные медицинское и военное ПО, ошибки в которых могут влиять на жизни людей; во-вторых, прикладное и промышленное ПО, и це-на ошибок в этих приложениях может стоить существенных денежных потерь, и, наконец, любительские приложения, ошибки которых влия-ют на настроение пользователей. Отметим, что количество критически важного ПО нарастает и, по факту, требования к нему увеличивают-ся. Одной из методик проверки качества и надежности кода является символьное исполнение [3].
- сожалению, символьное исполнение имеет свои ограничения. Для произвольной программы оно может свидетельствовать о наличии оши-бок, но не способно доказать их отсутствие. Причиной этому является очень большое число путей исполнения программы и, следовательно, огромное число символьных состояний. Примерами не очень больших программ, порождающих, тем не менее, очень большое количество сим-вольных состояний, является программа с циклом, количество итера-ций которого заранее неизвестно [6]. Однако даже если искусственно ограничивать количество посещений цикла, символьное исполнение бу-дет столкнётся с комбинаторным взрывом множества состояний, что ограничивает эффективность этой технологии на практике.
Комбинаторный взрыв множества путей исполнения является также помехой для обратного символьного исполнения [7], которое начинается из заданной точки программы и двигается в сторону начальной точки входа в программу. Обратное символьное исполнение необходимо, на-пример, для генерации полного тестового покрытия веток программы. Отчасти справится с проблемой роста множества состояний помога-ет использование различных стратегий исследования кода. Стратегия исследования — это функция, котор
Характеристики курсовой работы
Учебное заведение
Семестр
Просмотров
1
Размер
445,5 Kb
Список файлов
Направляемое свойством символьное исполнение программ на платформе .NET.doc
Комментарии
Нет комментариев
Стань первым, кто что-нибудь напишет!
СПбГУ
Tortuga
















