Бурдонов И.Б., Косачев А.С., Кулямин В.В. Теория соответствия для систем с блокировками и разрушением

М. : Институт системного программирования, 2006. — 494 с.Аннотация
В работе изучается тестирование соответствия систем, в которых возможна блокировка (приёма) стимулов и разрушение системы. Дивергенция также моделируется разрушением. В качестве соответствия предлагается отношение iocoβγδ – обобщение отношения ioco (Input-Output COnformance). Для того, чтобы избегать разрушения реализации при тестировании, отношение строится только на безопасных трассах, которые не могут привести к разрушению. Предлагается гипотеза о безопасности, определяющая класс реализаций, которые можно тестировать на соответствие заданной спецификации. Рассматриваются два вида моделей: трассовые модели и система переходов (Labelled Transition System), и показывается их эквивалентность. Описывается генерация тестов и её алгоритмизация. Рассматриваются различные виды пополнения частично-определённых по стимулам спецификаций. Сравниваются семантики отношений ioco и iocoβγδ. Рассматривается проблема несохранения соответствия при композиции и предлагается её решение с помощью монотонного преобразования спецификаций. Излагается общая теория монотонности соответствия и определяются достаточные условия монотонности. Предлагаются монотонные преобразования для общего случая и для подклассов без блокировок и/или разрушения. Рассматриваются проблемы алгоритмизации преобразований и композиции и описываются соответствующие алгоритмы.Содержание
Предисловие
Как читать эту книгу
Общематематические понятия и обозначения
Введение
Формализация понятия «правильности»
Функциональность
Взаимодействие
Аналитическая верификация и тестирование
Формальные спецификации
Математическая модель
Проблема извлечения модели
Тестовые возможности и гипотезы о реализации
Формализация тестового эксперимента
Машина тестирования
Разрешение тупиков (θ-наблюдение). Отказы
Разрушение (forbidden action)
Приоритеты
Дивергенция и недетерминизм
Проблема дивергенции
Проблема недетерминизма реализации
Недетерминизм спецификации
Трассовая и автоматная модели
Трассовая модель
Автоматная модель
Тесты
Трассовые тесты
Автоматные тесты. Синхронное и асинхронное тестирование
Безопасность тестирования
Проблема полноты тестирования
Модели ввода-вывода
Минимальные тестовые возможности.
Модели без блокировок стимулов
Отношение iocoβγδ
Проблемы взаимодействия тестера и реализации
Проблема блокировки стимулов
Проблема стимулов «на выбор»
Проблема реакций «на выбор».
Проблема «торможения» реакций
Пополнение спецификации
Неспецифицированный стимул
Допущение полноты (подразумеваемое пополнение)
Проблема рефлексивности соответствия
Асинхронное тестирование и верификация композиции
Две проблемы асинхронного тестирования
Безопасность при асинхронном тестировании
Дивергенция при асинхронном тестировании
Проблема монотонности соответствия при композиции.
Синхронное тестирование
Машина тестирования
Машина общего вида
Машина для iocoβγδ-тестирования – βγδ-машина
Трассовые модели
βγδ -модель
Разложение βγδ -модели на поддеревья
Модель безопасных трасс
Модель финальных трасс
Соотношение трассовых моделей
Гипотеза о безопасности
Соответствие iocoβγδ
Тест и полный набор тестов
Алгоритмизация
LTS-модель
Определение LTS
LTS-модель
LTS-модель как βγδ -машина
Эквивалентность βγδ -моделей и LTS-моделей
Гипотеза о безопасности и соответствие iocoβγδ
Композиция LTS и тесты
Алгоритмизация
Сравнение моделей
Сравнение трассовых моделей и LTS-модели
Сравнение моделей безопасных и финальных трасс с βγδ -моделью
Дивергенция вместо разрушения. Модель строго-конвергентных трасс
Различение разрушения и дивергенции
Пополнение спецификации
Пополнение состояний
Трассовое пополнение
Классическая семантика ioco
Алгоритмизация
Верификация композицииОбщая теория монотонности
Косая композиция и монотонное соответствие
Восемь достаточных условий монотонности соответствия
План доказательства достаточных условий
Мажорирование βγδ-трасс и отношение iocoβγδ
Мажорирование βγδ-трасс
Эквивалентность iocoβγδ мажорированию βγδ-трасс (Монотонность 1:)
φ-трассы
φ-символы, φ-трассы и φ-маршруты LTS
ξ -оператор. Генеративность φ-трасс (Монотонность 2:)
Композиция φ-трасс. Аддитивность (Монотонность 3:)
Общий случай: Мажорирование φ-трасс
Определение мажорирования φ-трасс
Мажорирование φ-трасс предпорядок (Монотонность 8:)
Генеративность мажорирования φ-трасс (Монотонность 4:)
Композиционность мажорирования φ-трасс (Монотонность 5:)
Общий случай: Преобразование Tβγδ
Примеры и общая идея преобразования
Формальное определение преобразования
Конформность преобразования (Монотонность 6:)
S-ветвящиеся и локально-конечно-ветвящиеся LTS
Мажорантность преобразования (Монотонность 7:)
Монотонность преобразования
Оптимизация преобразования
Общий случай: Алгоритмизация
Замкнутость по алгоритмическому преобразованию Tβγδ
Алгоритмизация преобразования Tβγδ для конечного алфавита
Алгоритмическое преобразование Tβγδ при многократной композиции
Алфавит и ветвление при композиции LTS
Проблема дивергенции
Слабо-регулярность и Tβγδ-преобразование. Сильно-регулярность
Двойная LTS и Wβγδ-преобразование.
Алгоритмизация композиции Tβγδ-преобразованных LTS
Алгоритмизация композиции Wβγδ-преобразованных LTS
Верификация композиции в частных случаях
Спецификации без разрушения
Мажорирование φ-трасс без разрушения
Преобразование Tβδ
Алгоритмизация
Спецификации без блокировок
Определение мажорирования φ-трасс
Мажорирование φ-трасс предпорядок (Монотонность 8:)
Генеративность мажорирования φ-трасс (Монотонность 4:)
Композиционность мажорирования φ-трасс (Монотонность 5:)
Преобразование Tγδ 335
4.2.6. Конформность преобразования Tγδ (Монотонность 6:)
Мажорантность преобразования Tγδ (Монотонность 7:)
Монотонность преобразования Tγδ
Алгоритмизация
Спецификации без блокировок и без разрушения
Монотонность
Алгоритмизация
Итоги и перспективы
Литература
Приложение: Доказательства утверждений