В данной работе описывается процесс разработки веб-интерфейса для верификатора Spin с возможностью интерактивного конструиро­вания конечных автоматов. Охватываются следующие этапы цикла разработки программного обеспечения: анализ, проектирование, реализация и тестирование.Кроме того, производится обзор популярных решений для формальной верификации программных систем и ихс равнение по введен­ным критериям.

• ВВЕДЕНИЕ
• 1. Анализ подходов
  • 1.1. Проверка моделей
  • 1.2. Темпоральные логики
    • 1.2.1. Темпоральная логика линейного времени LTL
    • 1.2.2. Темпоральная логика ветвящегося времени CTL
    • 1.2.3. Временная темпоральная логика ветвящегося времени TCTL
    • 1.2.4. Расширенная темпоральная логика ветвящегося времени CTL*
  • 1.3. Сравнительный анализ подходов к проверке моделей
    • 1.3.1. Cadence SMV
    • 1.3.2. NuSMV
    • 1.3.3. UPPAAL
    • 1.3.4. HyTech
    • 1.3.5. Spin
  • 1.4. Вывод
• 2. Постановка задачи
  • 2.1. Назначение и цели создания интерфейса
  • 2.2. Требования к программному обеспечению
    • 2.2.1. Серверное программное обеспечение
    • 2.2.2. Клиентское программное обеспечение
  • 2.3. Требования к оформлению и верстке страниц
  • 2.4. Функциональные возможности
    • 2.4.1. Режим редактирования
    • 2.4.2. Режим конструктора
  • 2.5. Требования к производительности
  • 2.6. Вывод
• 3. Проектирование архитектуры системы
  • 3.1. Клиент-серверное взаимодействие
  • 3.2. Режимы работы
  • 3.3. Серверная часть
    • 3.3.1. Проверка целостности и корректности клиентского запроса
    • 3.3.2. Подготовка к запуску верификатора Spin
  • 3.4. Клиентская часть
    • 3.4.1. Функциональные блоки
    • 3.4.2. Конструктор конечных автоматов
  • 3.5. Вывод
• 4. Разработка системы
  • 4.1. Используемый стек технологий
    • 4.1.1. Серверные технологии
    • 4.1.2. Клиентские технологии
  • 4.2. Сервер
    • 4.2.1. Система журналирования
    • 4.2.2. Подготовка к запуску верификатора Spin
    • 4.2.3. Запуск процессов
  • 4.3. Клиент
    • 4.3.1. Система журналирования
    • 4.3.2. Основные модули
    • 4.3.3. Конструктор
    • 4.3.4. Дизайн
  • 4.4. Вывод
• 5. Тестирование системы
  • 5.1. Определение тестируемых компонентов
  • 5.2. Тестирование сервера
    • 5.2.1. Тестирование проверок корректности клиентского запроса
  • 5.3. Тестирование клиента
    • 5.3.1. Тестирование команд конструктора
    • 5.3.2. Тестирование преобразования конечных автоматов в текстовое представление
    • 5.3.3. Тестирование производительности
  • 5.4. Вывод
• ЗАКЛЮЧЕНИЕ
• СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ
• ПРИЛОЖЕНИЕ А. СРАВНИТЕЛЬНЫЙ АНАЛИЗ ПОДХОДОВ К ПРОВЕРКЕ МОДЕЛЕЙ
• ПРИЛОЖЕНИЕ Б. РЕАЛИЗАЦИЯ СЕРВЕРА
• ПРИЛОЖЕНИЕ В. РЕАЛИЗАЦИЯ КЛИЕНТА
• ПРИЛОЖЕНИЕ Г. ТЕСТИРОВАНИЕ