Студопедия
Случайная страница | ТОМ-1 | ТОМ-2 | ТОМ-3
АрхитектураБиологияГеографияДругоеИностранные языки
ИнформатикаИсторияКультураЛитератураМатематика
МедицинаМеханикаОбразованиеОхрана трудаПедагогика
ПолитикаПравоПрограммированиеПсихологияРелигия
СоциологияСпортСтроительствоФизикаФилософия
ФинансыХимияЭкологияЭкономикаЭлектроника

Кумекин, Рыженков

ВВЕДЕНИЕ.

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 Использование формальных описателей в качестве спецификаций триггеров и триггерных связок.

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.10 Восстановление описателей по триггерным связкам.

3.2.11 Сравнение описателей.

 


Дата добавления: 2015-10-24; просмотров: 36 | Нарушение авторских прав


<== предыдущая страница | следующая страница ==>
Самородский,Иванин| МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РЕСПУБЛИКИ КАЗАХСТАН

mybiblioteka.su - 2015-2024 год. (0.007 сек.)