Міністерство освіти І науки україни icon

Міністерство освіти І науки україни




Скачати 74.63 Kb.
НазваМіністерство освіти І науки україни
Дата11.08.2012
Розмір74.63 Kb.
ТипДокументи

МІНІСТЕРСТВО ОСВІТИ І НАУКИ УКРАЇНИ

НаціональнИЙ авіаційнИЙ університет


ІНСТИТУТ НОВІТНІХ ТЕХНОЛОГІЙ



Індекс Н - № - 2



“Затверджую”

Проректор університету

з навчальної роботи

________________ Кулик М.С.

“____”_____________ 2007р.




НАВЧАЛЬНА ПРОГРАМА



з дисципліни: Доказове проектування

алгоритмів функціонування

реактивних систем

Спецкурс д.т.н. Чеботарьова А.М. (Інститут кібернетики НАН України)



Усього годин – 303

в тому числі аудиторних – 198

іспит – 3, 4 семестр










Київ - 2007



Навчальна програма дисципліни "Доказове проектування алгоритмів функціонування реактивних систем" складена на основі робочого навчального плану ІНТ (для технічних спеціальностей), затвердженого “______”_____________2007 р.


Навчальну програму склав:

докт.техн.наук Чеботарьов Анатолій Миколайович


Навчальна програма обговорена і ухвалена на засіданні науково-методичної редакційної ради ІНТ, протокол № від “____”_________2007року


Голова НМРР ________________ Кузнєцова О.Я.





“Згоден”

Декан ІНТ

______________ О.Я. Кузнєцова

“____” __________ 2007 р.



“Згоден”

Директор ІНТ

______________ В.В. Куліш

“____” __________ 2007 р.















^ 1. Пояснювальна записка


Основна мета дисципліни “ Доказове проектування алгоритмів функціонування реактивних систем" є формування системи знань і умінь щодо коректного проектування алгоритмів функціонування систем реального часу на основі сучасних методів специфікації вимог до функціонування систем, синтезу процедурного подання алгоритму, та формальної верифікації алгоритмів.


Задачі вивчення дисципліни:

  • здобуття загальної математичної підготовки, необхідної для опанування сучасних методів коректного проектування алгоритмів реального часу (реактивних алгоритмів);

  • знайомство з основними математичними моделями, що використовуються для опису властивостей та функціонування систем у часі;

  • оволодіння навичками специфікації вимог до функціонування систем реального часу;

  • набуття знань щодо методів синтезу процедурного подання реактивних алгоритмів, виходячи із специфікації вимог до них у логічній мові першого порядку;

  • знайомство з новітніми технологіями синтезу алгоритмів на базі системи доказового проектування Dual та системи MVSIS;

  • знайомство з сучасними методами представлення даних у системах автоматизованого проектування алгоритмів.


В результаті вивчення дисципліни студент повинен знати:

  • різновиди моделей, що використовуються при розв’язанні задач специфікації, синтезу та верифікації алгоритмів реального часу, зокрема, різновиди автоматів-перетворювачів та автоматів-розпізнавачів;

  • основні логічні мови, що використовуються для специфікації вимог до функціонування алгоритму та його властивостей, зокрема, мови, що побудовані на основі числення предикатів першого порядку, темпоральних логік та числення на базі операторів нерухомої точки;

  • загальні принципи побудови формальної специфікації властивостей алгоритму;

  • основні задачі, що розв’язуються в процесі синтезу відкритих систем з урахуванням їх взаємодії з оточуючим середовищем;

  • методи перевірки несуперечності вихідної специфікації у логічній мові першого порядку;

  • методи перевірки узгодженості автоматів;

  • основні принципи формальної верифікації алгоритмів (формулювання проблеми та основні підходи до її розв’язання).


Студент повинен вміти:

  • користуватися різними формами подання скінченних автоматів при формулюванні та розв’язанні інженерних задач проектування алгоритмів реального часу;

  • специфікувати у логічній мові першого порядку та темпоральних логіках властивості дискретних пристроїв;

  • перевіряти несуперечність специфікацій як вручну для нескладних випадків, так і за допомогою системи Dual для специфікацій реальних пристроїв;

  • аналізувати результати синтезу, одержані за допомогою систем Dual та MVSIS.



^

2. Зміст навчальної дисципліни


Тема 1. Функціональна специфікація реактивного алгоритму.

Функціональна модель алгоритму. Структура специфікації. Монадична логіка предикатів першого порядку. Інтерпретація мов специфікації над множиною цілих чисел. Класифікація надслів. Надсловарна семантика мови L. Мови Lmax та L*. Автоматна семантика мов специфікації. Перехід від мови L* до L.


Тема 2. Властивості L-специфікацій.

Простір станів для t–формули. Представлення t–формули у просторі станів. Мінімальна форма специфікації. Побудова мінімальної форми. Необхідні та достатні умови специфікації детермінованого всюди визначеного автомата. Стандартні форми специфікації детермінованих всюди визначених автоматів. Стандартна форма специфікації детермінованого автомата. Специфікація у вигляді необхідних умов зміни значення предиката. Необхідні умови частковості специфікації.


Тема 3. Темпоральні логіки.

Класифікація темпоральних логік. Логіки з лінійним часом. Синтаксис та семантика логіки LTL. Логіка з розгалуженим часом. Структури Кріпке. Синтаксис та семантика логік CTL та CTL*. Виразні можливості темпоральних логік. -мови. Властивості -мов. Автомати Бюхі. Безлічильникові автомати.


Тема 4. Властивості реактивних систем.

Неформальне визначення властивостей «безпеки» та «життєздатності». Формальне визначення властивостей безпеки (safety) та життєздатності (liveness). Властивості, що визначаються формулами мов L та L*. Топологічна характеризація властивостей. Борелевська ієрархія топологічних класів властивостей. Відношення симуляції на структурах Кріпке. Відношення бісимуляції. Властивості відношення бісимуляції. Еквівалентні перетворення структур Кріпке.


Тема 5. Числення на базі операторів нерухомої точки..

Часткові порядки. Решітки. Монотонні та неперервні функції. Поняття нерухомої точки. Частковий порядок на множині усіх множин надслів у заданому алфавіті. Найменша й найбільша нерухомі точки. Теорема Кнастера-Тарського про нерухому точку. Методи обчислення нерухомих точок. Мова -числення. Синтаксис та семантика -числення. Нормальні форми формул -числення.


Тема 6. Проблеми синтезу відкритих систем.

Поняття відкритої та замкнутої системи. Реалізованість відкритої системи. Існуючи підходи до розв’язання проблеми синтезу відкритих систем. Нескінченне відмічене дерево. Мови дерев. Автомати Рабіна над деревами. Проблема порожності мови дерев. Ігровий підхід до розв’язання проблеми порожності мови дерев. Детермінованість гри. Проблема доповнення мови дерев. Зведення проблеми реалізації відкритої системи до проблеми порожності мови автомата Рабіна.


Тема 7. Ігрові стратегії розв’язання проблеми синтезу.

Ігрова структура. Поточний стан ігрової структури. Поняття гри. Стратегія гри. Узгодженість гри зі стратегією. Виграшна стратегія. Ігрова структура, що відповідає специфікації. Транзиційна система. Поняття реакції транзиційної системи. Виконуваність специфікації на транзиційній системі. Темпоральна семантика транзиційної системи. -числення, визначене на ігрових структурах. Обчислення виграшної стратегії на базі обчислення нерухомої точки відповідного функціоналу. Побудова транзиційної системи, що реалізує специфікацію.


Тема 8. Узгодженість автоматів.

Узгодженість автоматів як необхідна умова реалізованості відкритої системи. Циклічна композиція автоматів. Симетрична циклічна композиція автоматів Мура. Права циклічна композиція. Лема про еквівалентність композицій. Визначення узгодженості детермінованих автоматів. Поняття циклічної детермінізації недетермінованого автомата. Взаємна узгодженість не детермінованих автоматів. Узгодженість одного недетермінованого автомата Мура з іншим.


Тема 9. Теореми про узгодженість автоматів.

Автомати із скінченною пам’яттю. -нормальная форма автомата із скінченною пам’яттю. Необхідні та достатні умови узгодженості одного автомата з другим. Відповідні умови в термінах правої циклічної композиції. Поняття закритого стану для правої циклічної композиції. Лівий зсув автомата за входами. Паралельна циклічна композиція автоматів. Теорема про ізоморфізм ядер правої та паралельної циклічної композиції. Необхідні та достатні умови узгодженості в термінах паралельної композиції. Поняття закритого стану для паралельної композиції. Алгоритм визначення узгодженості на базі вилучення закритих станів.


Тема 10. Методи перевірки узгодженості специфікацій у мові L.

Представлення специфікацій у вигляді множин диз’юнктів. Перетин специфікацій. Лівий зсув множини диз’юнктів. Частковість стану автомата. Диз’юнкти першого та другого роду. Необхідна умова частковості автомата, що специфікується. Умова вилучення закритого стану. Резолюційний підхід до перевірки узгодженості специфікацій. Процедура вилучення закритих станів. Метод роздільної резолюції.

^

3. Основна рекомендована література





  1. Капітонова Ю.В., Кривий С.Л., Летичевський О.А., Луцький Г.М., Печурін М.К. Основи дискретної математики. Київ: «Наукова думка», 2002. – 579 с.

  2. Глушков В.М. Синтез цифровых автоматов. М.: Физматгиз, 1962.– 476 с.

  3. Кобринский Н.Е., Трахтенброт Б.А. Введение в теорию конечных автоматов. М.: Физматгиз, 1962. – 494 с.

  4. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983. – 360 с.

  5. Тейз А., Грибомон П., Луи Ж. и др. Логический подход к искусственному интеллекту. От классической логики к логическому программированию. М.: «Мир», 1990. – 432 с.

  6. Тейз А., Грибомон П., Юлен Г. и др. Логический подход к искусственному интеллекту. От модальной логики к логике баз данных. М.: «Мир», 1998. – 494 с.

  7. Кларк Э.М. мл., Грамберг О., Пелед Д. Верификация моделей программ: Model checking. Пер. с англ. М.: МЦНМО, 2002. – 416 с.

  8. Кривий С.Л. Дискретна математика. Київ: Видавничий дім «Києво-Могилянська академія», 2007. – 570 с.

Схожі:

Міністерство освіти І науки україни iconПоложення про нагородження нагрудним знаком "А. С. Макаренко" Міністерства освіти І науки України
Міністерству освіти І науки України Міністерство освіти І науки Автономної Республіки Крим, управління освіти І науки обласних, Київської...
Міністерство освіти І науки україни iconПоложення про нагородження нагрудним знаком "Василь Сухомлинський" Міністерства освіти І науки України
Міністерству освіти І науки України Міністерство освіти І науки Автономної Республіки Крим, управління освіти І науки обласних, Київської...
Міністерство освіти І науки україни iconПоложення про нагородження нагрудним знаком "Софія Русова" Міністерства освіти І науки України
Міністерству освіти І науки України Міністерство освіти І науки Автономної Республіки Крим, управління освіти І науки обласних, Київської...
Міністерство освіти І науки україни iconРішення про нагородження Нагрудним знаком ухвалюється Колегією Міністерства освіти І науки України, затверджується наказом Міністра І публікується в газеті "Освіта України"
Міністерству освіти І науки України Міністерство освіти І науки Автономної Республіки Крим, управління освіти І науки обласних, Київської...
Міністерство освіти І науки україни iconРішення про нагородження Нагрудним знаком ухвалюється Колегією Міністерства освіти І науки України, затверджується наказом Міністра І публікується в газеті "Освіта України"
Міністерству освіти І науки України Міністерство освіти І науки Автономної Республіки Крим, управління освіти І науки обласних, Київської...
Міністерство освіти І науки україни iconРішення про нагородження Нагрудним знаком ухвалюється Колегією Міністерства освіти І науки України, затверджується наказом Міністра І публікується в газеті "Освіта України"
Міністерству освіти І науки України Міністерство освіти І науки Автономної Республіки Крим, управління освіти І науки обласних, Київської...
Міністерство освіти І науки україни iconМіністерство освіти І науки україни 01135, м. Київ, проспект Перемоги
Міністерства освіти і науки України від 17. 04. 2009 року №341 «Про затвердження Плану дій щодо вдосконалення викладання дисципліни...
Міністерство освіти І науки україни iconПоложення про нагородження нагрудним знаком "Петро Могила" Міністерства освіти І науки України
Міністерство освіти І науки Автономної Республіки Крим, управління освіти І науки обласних, Київської І севастопольської міських...
Міністерство освіти І науки україни iconМіністерство освіти І науки україни пр. Перемоги
Міністерство освіти і науки Автономної Республіки Крим, управління (департаменти) освіти і науки обласних, Київської і Севастопольської...
Міністерство освіти І науки україни iconМіністерство освіти І науки україни пр. Перемоги
Міністерство освіти і науки, молоді та спорту Автономної Республіки Крим, управління (департаменти) освіти і науки обласних, Київської...
Міністерство освіти І науки україни iconМіністерство освіти І науки україни пр. Перемоги
Міністерство освіти і науки, молоді та спорту Автономної Республіки Крим, управління (департаменти) освіти і науки обласних, Київської...
Додайте кнопку на своєму сайті:
Документи


База даних захищена авторським правом ©zavantag.com 2000-2013
При копіюванні матеріалу обов'язкове зазначення активного посилання відкритою для індексації.
звернутися до адміністрації
Документи