Руководитель и консультанты дипломного проекта
Nbsp; МИНОБРНАУКИ РОССИИ Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования "Московский государственный технический университет радиотехники, электроники и автоматики" МГТУ МИРЭА Факультет информационных технологий (ИТ) БК №231 «Информационных процессов и систем» Международного центра по информатике и электронике (ИнтерЭВМ) Система менеджмента качества обучения СМКО МИРЭА 7.3/04.ЗДпр.2ВМС/О/230105 -13 УТВЕРЖДАЮ СОГЛАСОВАНО Декан факультета____________ А.Б. Петров Заведующий кафедрой_______________ А.В. Старовойтов «____» __________2013 г. «____» __________2013 г.
ЗАДАНИЕ
На выполнение дипломного проекта
Дипломник Фамилия Андрей Александрович
Специальность 230105.65 «Программное обеспечение ВТ и автоматизированных систем»
Группа ИТО-3-08
Шифр 081035
Тема дипломного проекта
Программные средства для автоматизации формальной верификации на основе трансляции UML-модели
Техническое задание на выполнение дипломного проекта
Разработать программное обеспечение для автоматизации генерации результирующей SMV-модели транслятора диаграмм состояний UML во входной язык верификатора SMV. Генератор SMV-модели должен обеспечивать корректное считывание UML-диаграмм состояний собственного формата из памяти транслятора диаграмм состояний UML во входной язык верификатора и его преобразование в SMV-код, который поддерживается программным комплексом NuSMV. Должны обрабатываться UML-диаграммы состояний любой сложности, состоящие из одного модуля Region. Генератор формул-ограничений должен обеспечивать генерацию файла ограничений из введенных параметров. Программное обеспечение должно быть кроссплатформенным.
|
|
|
Планируемые результаты выполнения дипломного проекта
Программные средства для автоматизации формальной верификации диаграмм состояний UML.
Этапы выполнения дипломного проекта
| № этапа | Содержание этапа работы | Результат выполнения этапа | Срок выполнения |
| 1. | Разработка разделов предпроектного исследования | Разделы предпроектного исследования | 15.02.2013 |
| 2. | Разработка технического задания | Разделы технического задания | 22.02.2013 |
| 3. | Разработка архитектуры транслятора | Архитектура транслятора | 15.03.2013 |
| 4. | Разработка архитектуры генератора SMV-модели и генератора формул | Архитектура генератора SMV-модели и ограничителя формул | 29.03.2013 |
| 5. | Разработка, отладка и тестирование программного обеспечения генератора SMV-модели и генератора формул | Готовое программное обеспечение | 05.04.2013 |
| 6. | Разработка экономического раздела | Экономический раздел | 26.04.2013 |
| 7. | Разработка разделов безопасности и экологичности | Разделы безопасности и экологичности | 03.05.2013 |
| 8. | Оформление РПЗ и графической части проекта. | Графические материалы и РПЗ | 04.06.2013 |
Содержание экономического раздела дипломного проекта
|
|
|
5.1 Расчет трудозатрат и составление сметы затрат на выполнение проекта
5.2 Разработка бизнес-плана и составление календарного графика выполнения проекта
5.3 Технико-экономическое обоснование целесообразности выполнения проекта
Экологичность и безопасность
Спроектировать оптимальные условия труда инженера-программиста
6.1 Анализ условий труда
6.2 Оптимальное рабочее место
6.3 Карта условий труда
6.4 Комбинированное естественное освещение
6.5 Аэрация
6.6 Оптимизация информационной нагрузки
Перечень разрабатываемых документов и графических материалов
7.1 Схема управления данными (блок-схема основных алгоритмов) – 2 листа
7.2 Схема связей данных (диаграмма вариантов использования генератора) – 1 лист
7.3 Схема потоков данных (структура программных средств) – 1 лист
7.4 Схема размещения данных (структура входного формата генератора) – 1 лист
|
|
|
7.5 Схема представления данных (интерфейс пользователя) – 1 лист
7.6 Схема представления данных (UML-диаграмма состояний) – 1 лист
7.7 Расчетно-пояснительная записка к дипломному проекту.
Практическая значимость дипломного проекта
Программные средства для автоматизации формальной верификации диаграмм состояний UML входят в состав транслятора диаграмм состояний UML во входной язык верификатора SMV. Транслятор диаграмм состояний UML во входной язык верификатора SMV может применяться для автоматизации процесса верификации UML-диаграмм состояний как в области проектирования аппаратных и программных средств (проверка правильности составления автоматной диаграммы, проверка алгоритма программы, отображенного на диаграмме состояний, на этапе проектирования), так и в области обучения.
Руководитель и консультанты дипломного проекта
Дата добавления: 2018-02-15; просмотров: 588; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!