СодержаниеМагистерская диссертация
Егоров К.В.
Васильев в.н.
По магистерской диссертации
Краткое содержание магистерской диссертации
Верификация применяется на стадиях вычисления функции приспособленности, мутации и скрещивания.
Результат верификации используется в процессе вычисления функции приспособленности, мутации и скрещивании особей генетического а
Экономическая часть (какие использованы методики, экономическая эффективность результатов)
Является ли работа продолжением курсовых проектов (работ), есть ли публикации
Практическая ценность работы. Рекомендации по внедрению
ГЛАВА 1.Верификация автоматных программ
Model Checking
Model Checking
Linear Temporal Logic, LTL
1.1.Язык логики линейного времени
1.2.Алгоритм верификации
LTL формулы на автомате Бюхи будем проверять, что пересечение верифицируемого автомата Бюхи и автомата Бюхи, соответствующего от
Depth-first search, DFS
1.3.Программная реализация верификатора
Выводы по главе 1
ГЛАВА 2.Описание предлагаемого метода
2.1.Представление конечного автомата в виде хромосомы генетического алгоритма
2.1.1.Обработка входных переменных
2.2.Вычисление функции приспособленности
LTL формулы можно только примерно. Если n
2.2.1.Учет результата верификации при вычислении функции приспособленности
2.3.Операция мутации
2.4.Операция скрещивания
2.4.1.Скрещивание с учетом результата верификации
2.5.Методика построения автоматных программ
Выводы по главе 2
ГЛАВА 3.Программная реализация метода и экспериментальное исследование
3.1.Программная реализация
UniMod xml описания модели. В результате, созданную автоматную модель можно сразу запускать в инструментальном средстве UniMod
3.2.Построение конечного автомата управления часами с будильником
3.2.1.Система тестовых примеров и темпоральных свойств
3.2.2.Результаты применения генетического алгоритма
3.3.Построение конечного автомата управления дверьми лифта
3.3.1.Система тестовых примеров
3.3.2.Результаты эксперимента
Выводы по главе 3
|
