Методы построения графо-аналитических моделей функциональных программ

• Автор: Лаздин, Артур Вячеславович
• Шифр специальности: 05.13.12
• Научная степень: Кандидатская
• Год защиты: 2009
• Место защиты: Санкт-Петербург
• Количество страниц: 141 с.

СОДЕРЖАНИЕ
СОДЕРЖАНИЕ
ВВЕДЕНИЕ

ГЛАВА 1. МЕТОДЫ КОНТРОЛЯ И АНАЛИЗА ПРОГРАММ.

1.1 Программа как объект исследования.

1.2 Методы контроля программ

1.2.1 Статический анализ программ

1.2.2 Динамический анализ программ.

I 2.3 Другие методы анализа

1.3 Место методов анализа в жизненном цикле ПО

1.4 Постановка задачи

Выводы
ГЛАВА 2. МЕТОД ВОССТАНОВЛЕНИЯ УПРАВЛЯЮЩЕГО ГРАФА ФУНКЦИОНАЛЬНОЙ ПРОГРАММЫ ПО ЕЕ ИСПОЛНЯЕМОМУ КОДУ.
2.1 Формальные модели программ.
2.2 Типы и структуры исполняемых модулей.
2.2.1 Обобщенный формат команды процессора
2.2 2 Графовое представление исполняемого кода.
2.2.3. Графоаналитическая модель исполняемого модуля.
2.3 Метод формирование управляющего графа функциональной программы.
2.4 Оценка степени сложности управляющего графа ФП.
Выводы
ГЛАВА 3. СТРУКТУРНОФУНКЦИОНАЛЬНАЯ ДЕКОМПОЗИЦИЯ УПРАВЛЯЮЩЕГО ГРАФА ФУНКЦИОНАЛЬНОЙ ПРОГРАММЫ.
3.1 Поиск процедур. Алгоритмы.
3.3. Поиск параметров процедур.
3.2 Поиск циклов. Алгоритмы.
3.4 Поиск параметров цикла.
3.5 Поиск инвариант цикла.
Выводы
ГЛАВА 4. ПРОГРАММНАЯ СИСТЕМА ВОССТАНОВЛЕНИЯ УПРАВЛЯЮЩЕГО ГРАФА ФУНКЦИОНАЛЬНОЙ ПРОГРАММЫ.
4.1 Общая структура программной системы.
4.2 Модуль имитатора загрузчика.
4.3 Модули дешифрации и поиска КУПК
4.5 Модуль формирования и сортировки списка вершин
4.6 Модули поиска процедур и циклов Ц
4.6 Модуль формирования матриц
4.7 Методика работы с программной системой
4 7 1 Чтение данных из заголовка исполняемого модуля.
4 7.2 Запись в файл дампа ИМ.
4.7.3 Дизассемблирование команд ИМ.
4.7.4 Формирование и сортировка предварительного списка вершин
4.7.5. Поиск адресов начала и конца всех процедур ИМ.
4.7.6 Поиск адресов начала и конца всех циклов ИМ и определение их вложенности.
4.7.7 Запуск программной системы
Выводы
ЗАКЛЮЧЕНИЕ
СПИСОК ЛИТЕРАТУРЫ


Большое внимание уделяется методам синтеза и анализа алгоритмов [,,,. V (набор переменных программы) в себя: V——>К. V, с набором значений в некотором фиксированном множестве. Анализ программы, следовательно, может осуществляться различными методами, и использование того или иного метода зависит не только от способа представления программы, но и от цели, которая ставится перед анализом. В качестве таких целей могут рассматриваться: доказательство правильности (верификация) программ, характер изменения множества состояний памяти, как в ходе выполнения программы, гак и по завершению ее работы, доказательство тех или иных свойств программ или доказательство теорем о программах. В подавляющем большинстве случаев контроль программ выполняется для определения двух характеристик программы: она должна быть правильной и безопасной. В настоящее время все чаще исследуется безопасность программ. Под безопасностью программного обеспечения (ПО) понимается отсутствие в коде исследуемой программы элементов разрушающих программные средства или недекларируемых возможностей. Главное отличие в постановке этой задачи от традиционных задач анализа 0 состоит в том, что анализу на безопасность подвергается непосредственно исполняемый код программы, а не ее алгоритм, спецификация или текст на языке высокого уровня. Выделяют две основных группы методов контроля и исследования программ: статические и динамические {,,,]. Под статическими понимаются такие методы, при которых исследуется текст программы независимо от его формы. Это может быть исследование исходных текстов, написанных на языках высокого уровня, на ассемблере или в кодах процессора. Динамические методы анализа работают с исполняемым кодом программы и основаны на анализе получаемых в ходе ее выполнения результатов. Рассмотрим эти методы подробнее. Статический анализ - это проверка программы по ее тексту (без выполнения) с помощью инструментальных средств без выполнения; причем под выполнением понимается как собственно прогоны исполняемого кода на реальной вычислительной машине, так и имитационное выполнение (эмуляция). Наиболее известной формой статического контроля является синтаксический контроль программы с помощью компилятора, при котором проверяется соответствие текста программы синтаксическим правилам языка программирования [,]. Вторая форма статического контроля - контроль структурированности программ, то есть проверка выполнения соглашений и ограничений структурного программирования. Примером подобной проверки может быть выявление в тексте программы ситуаций, когда цикл образуется с помощью оператора безусловного перехода (использования оператора вОТО для перехода вверх по тексту программы). Для проведения контроля структурированности могут быть созданы специальные инструментальные средства, а при их отсутствии эта форма статического контроля может совмещаться с визуальным контролем [,]. Третья форма статического контроля - контроль правдоподобия программы, то есть выявление в се тексте конструкций, которые хотя и синтаксически корректны, но, скорее всего, содержат ошибку или свидетельствуют о ней. Даже если присутствие в тексте программы неправдоподобных конструкций не приводит к ее неправильной работе, исправление этого фрагмента повысит ясность и эффективность программы, т. Четвертой формой статического контроля программ является их верификация, то есть аналитическое доказательство их корректности. Метод установления правильности программ при помощи строгих средств известен как верификация программ [2,5,8,,,,,]. Этот метод заключается в том, чтобы с помощью формальных математических методов показать, что программа удовлетворяет своим требованиям и сделать это вне зависимости от конкретных входных наборов. Использование методов верификации позволяет провести анализ работоспособности программы на всем диапазоне возможных входных значений, то есть, применение этих методов гарантирует корректность проектного решения относительно сформулированных для него фу и к цио нал ы іьтх специ фи каций.