ВВЕДЕНИЕ
1 АНАЛИЗ СОВРЕМЕННЫХ МЕТОДОВ И СРЕДСТВ ВЕРИФИКАЦИИ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ И БАЗ ДАННЫХ
1.1 Архитектура современных реляционных баз данных.
1.2 Формирование концепции целостности реляционных баз данных
1.2.1 Понятие целостности реляционных баз данных.
1.2.2 Определение места целостности в системе характеристик качества баз данных
1.2.3 Анализ механизмов реализации требований целостности в реляционных базах данных
1.3 Общая характеристика методов и инструментов верификации программного обеспечения и баз данных.
1.3.1 Понятие, цели и задачи верификации.
1.3.2 Классификация методов верификации программного обеспечения
1.3.3 Современные методы и инструменты верификации реляционных баз данных
1.4 Анализ эффективности динамического тестирования целостности реляционных баз данных
1.5 Постановка задач исследования
2 РАЗРАБОТКА МЕТАМОДЕЛИ ТРЕБОВАНИЙ И ФУНКЦИЙ ЦЕЛОСТНОСТИ РЕЛЯЦИОННЫХ БАЗ ДАННЫХ.
2.1 Целостность как корректность состояний и переходов.
2.2 Разработка метамодели требований целостности на основе совершенствования метамодели ГарсиаМолина, Ульмана и Уидом.
2.3 Применение формальных описателей в качестве спецификаций объектов
ограничений.
2.3.1 Типовые требования целостности и их формальные описатели.
2.3.2 Использование формальных описателей в качестве спецификаций
триггеров и триггерных связок.
2.4 Выводы
3 РАЗРАБОТКА МЕТОДА ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ И ВЫЯВЛЕНИЯ НЕДЕКЛАРИРОВАННЫХ ВОЗМОЖНОСТЕЙ ОБЪЕКТОВОГРАНИЧЕНИЙ РЕЛЯЦИОННЫХ БАЗ ДАННЫХ.
3.1 Анализ методов логикоалгебраической верификации программных процедур
3.1.1 Связь между формальным описателем требования целостности и тройкой Хоара.
3.1.2 Взаимосвязь функциональной корректности программы с выбором наиболее сильного постусловия.
3.1.3 Анализ возможности применения метода индуктивных утверждений для верификации триггеров.
3.1.4 Требования к разрабатываемому методу формальной верификации
объектовограничений
3.2 Разработка процедур и алгоритмов, используемых в рамках метода формальной верификации объектовограничений.
3.2.1 Этапы проведения верификации
3.2.2 Восстановление описателей по ограничениям целостности.
3.2.3 Восстановление описателей по триггерам
3.2.4 Получение собственных постусловий простых операторов
3.2.5 Усиление собственного постусловия простого оператора
3.2.6 Правило последовательного усиления постусловий операторов маршрута
3.2.7 Получение постусловия маршрута, содержащего оператор отката транзакции
3.2.8 Алгоритм синтеза постусловия маршрута.
3.2.9 Синтез постусловия триггера.
3.2. Восстановление описателей по триггерным связкам
3.2. Сравнение описателей.
3.3 Выводы
4 РАЗРАБОТКА РЕКОМЕНДАЦИЙ ПО ПРАКТИЧЕСКОМУ ПРИМЕНЕНИЮ МЕТОДА ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ ОБЪЕКТОВОГРАНИЧЕНИЙ РЕЛЯЦИОННЫХ БАЗ ДАННЫХ
4.1 Границы применимости разработанного метода формальной верификации объектовограничений.
4.2 Основные принципы построения и функционирования программной системы проведения верификации объектовограничений
4.2.1 Описание функций системы проведения верификации
4.2.2 Структура системы проведения верификации объектовограничений.
4.3 Описание программной реализации системы проведения верификации объектовограничений.
4.3.1 Описание реализации подсистемыкоординатора
4.3.2 Описание реализации подсистемы анализа Ькодов.
4.3.3 Описание реализации подсистемы анализа спецификаций
4.3.4 Описание реализации подсистемы восстановления описателей
4.3.5 Описание реализации подсистемы сравнения описателей
4.4 Оценка оперативности и полноты выявления недекларированных возможностей в объектахограничениях с использованием разработанного метода.
4.5 Выводы.
ЗАКЛЮЧЕНИЕ.
СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ
- Київ+380960830922