Table | Card | RUSMARC | |
Allowed Actions: –
Action 'Read' will be available if you login or access site from another network
Action 'Download' will be available if you login or access site from another network
Group: Anonymous Network: Internet |
Annotation
В данной работе описывается процесс разработки веб-интерфейса для верификатора Spin с возможностью интерактивного конструирования конечных автоматов. Охватываются следующие этапы цикла разработки программного обеспечения: анализ, проектирование, реализация и тестирование.Кроме того, производится обзор популярных решений для формальной верификации программных систем и ихс равнение по введенным критериям.
Document access rights
Network | User group | Action | ||||
---|---|---|---|---|---|---|
ILC SPbPU Local Network | All | |||||
Internet | Authorized users SPbPU | |||||
Internet | Anonymous |
Table of Contents
- ВВЕДЕНИЕ
- 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. Вывод
- 4.1. Используемый стек технологий
- 5. Тестирование системы
- 5.1. Определение тестируемых компонентов
- 5.2. Тестирование сервера
- 5.2.1. Тестирование проверок корректности клиентского запроса
- 5.3. Тестирование клиента
- 5.3.1. Тестирование команд конструктора
- 5.3.2. Тестирование преобразования конечных автоматов в текстовое представление
- 5.3.3. Тестирование производительности
- 5.4. Вывод
- ЗАКЛЮЧЕНИЕ
- СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ
- ПРИЛОЖЕНИЕ А. СРАВНИТЕЛЬНЫЙ АНАЛИЗ ПОДХОДОВ К ПРОВЕРКЕ МОДЕЛЕЙ
- ПРИЛОЖЕНИЕ Б. РЕАЛИЗАЦИЯ СЕРВЕРА
- ПРИЛОЖЕНИЕ В. РЕАЛИЗАЦИЯ КЛИЕНТА
- ПРИЛОЖЕНИЕ Г. ТЕСТИРОВАНИЕ
Usage statistics
Access count: 435
Last 30 days: 0 Detailed usage statistics |