Програма для студентів спеціальності 04030201 "Інформатика" Затверджено



Скачати 169.4 Kb.
Дата конвертації09.04.2017
Розмір169.4 Kb.
Київський національний університет імені Тараса Шевченка
Факультет кібернетики

Кафедра теорії та технології програмування


Укладач: Доктор фіз.-мат. наук, професор Дорошенко А.Ю.

ВЕРИФІКАЦІЯ І ВАЛІДАЦІЯ ПРОГРАМНИХ СИСТЕМ

Робоча навчальна програма

для студентів спеціальності 8.04030201 “Інформатика”

Затверджено

на засіданні кафедри теорії та технології програмування

Протокол № 10

від ”25” травня 2012 р.


Зав. кафедри

теорії та технології програмування

Нікітченко М.С.

Затверджено

на засіданні Вченої ради факультету кібернетики

Протокол № 9

від ”28” травня 2012 р.


Декан факультету кібернетики

Анісімов А.В.


КИЇВ-2012

Робоча навчальна програма з дисципліни

“Верифікація і валідація програмних систем”

Укладач: доктор фіз.-мат. наук, професор Дорошенко Анатолій Юхимович

Лектор: доктор фіз.-мат. наук, професор Дорошенко А.Ю.




Погоджено

з науково-методичною комісією

“___” _______________ 2012 р.

Голова НМК факультету

Хусаїнов Д.Я

ВСТУП

Дисципліна "Верифікація і валідація програмних систем " є нормативною дисципліною спеціальності "Інформатика", що викладається в 3 семестрі магістерської програми в обсязі 3 кредитів; загальний обсяг годин 108, з них 34 години лекційних занять, 17 лабораторних, 57 годин самостійної роботи. Закінчується курс іспитом у 3 семестрі магістерської програми.



Метою і завданням навчальної дисципліни "Верифікація і валідація програмних систем" є засвоєння техніки перевірки правильності програм шляхом побудови моделей програм з подальшим доведенням властивості побудованих моделей, що характеризують її правильність. Визначення понять верифікації і валідації програмних систем здійснюється з використанням основ математичної логіки і теорії алгоритмів дає необхідні знання для обгрунтування правильності алгоритмів і є невід’ємною частиною науки програмування. Апарат верифікації і валідації програмних систем може бути практичним інструментом доведення правильності прикладних алгоритмів у різноманітних предметних областях, створення сучасних програмних та інформаційних систем.

Предмет навчальної дисципліни "Верифікація і валідація програмних систем" включає в себе вивчення методів перевірки правильності та тестування програм, методів доведення правильності програм. Це робиться шляхом побудови моделей програм з подальшим доведенням властивості побудованих моделей, що характеризують її правильність.

Вимоги до знань та вмінь. Для засвоєння курсу базовими дисциплінами є: математичний аналіз, програмування, теорія алгоритмів і математична логіка.

Місце в структурно-логічній схемі спеціальності. Нормативна навчальна дисципліна "Верифікація і валідація програмних систем" є складовою циклу професійної підготовки фахівців освітньо-кваліфікаційного рівня "магістр". Цей курс потрібен для глибшого вивчення нормативних дисциплін магістерської програми з системного програмування та інформаційних технологій, а також низки спецкурсів відповідного напряму.
Контроль знань здійснюється за модульно-рейтинговою системою.

Робота в семестрі розділена на 3 змістових модулі. Результати навчальної діяльності студентів оцінюються за 100-бальною шкалою.

Семестрова оцінка – 65 балів; із них модульні контрольні роботи – 30 балів, активна робота студентів – 15 балів, колоквіум – 20 балів. Підсумкова екзаменаційна робота – 35 балів. Максимальна підсумкова оцінка – 100 балів.

Порядок розрахунку загальної оцінки.

Модульні контрольні роботи – 30 = 10+10+10 балів.

За активну роботу студента на лабораторних заняттях та на самостійній роботі до семестрової оцінки може бути додано до 15 балів.

Студент має право на одне перескладання модульної контрольної роботи із можливістю отримання максимальної кількості балів 10.

Термін перескладання визначається викладачем.

Розрахунок балів по модулях:

Модуль 1: 15 балів (модульна контрольна робота– 10, за активну роботу – 5).

Модуль 2: 15 балів (модульна контрольна робота – 10, за активну роботу – 5).

Модуль 3: 15 балів (модульна контрольна робота – 10, за активну роботу – 5).

Студент допускається до складання іспиту, якщо кількість набраних за семестр балів не менше 30.



Шкала оцінювання

100-бальна система

Національна шкала

90-100

Відмінно

5

85-89

Добре

4

75-84

65-74

Задовільно

3

60-64

35-59

не задовільно

2

1-34

не задовільно

1

ТЕМАТИЧНИЙ ПЛАН ЛЕКЦІЙ


№ лекції

Назва лекції

Кількість годин

Лекції

Лабораторні

Самостійна робота




Змістовий модуль 1. Життєвий цикл розробки програмного забезпечення (ПЗ)










1

Проблема розробки програмного програмного забезпечення

2




2

2

Життєвий цикл ПЗ та методології розробки життєвого циклу ПЗ.

2

2

3




Модульна контрольна робота













Колоквіум













Змістовий модуль 2. Методи перевірки правильності та тестування програм










3

Інженерія вимог до ПЗ

2




4

4

Поняття верифікації і валідації програмного забезпечення

2

2

4

5

Класифікація відмов та помилок у ПЗ.

2




2

6

Основні поняття та методи тестування програм

2




4

7

Процеси тестування програмних систем

2

2

2




Модульна контрольна робота













Змістовий модуль 3. Методи доведення правильності програм










8

Формальне моделювання програмних систем

2




4

9

Методи доведення правильності програм

2

2

4

10

Логічні засоби специфікацій програм

2




4

11

Перевірка формул на моделі

2

2

2

12

Двійкові діаграми рішень

2




4

13

Символьна верифікація моделей

2

2

2

14

Процеси верифікації ПЗ

2




4

15

Інспекційні методи верифікації ПЗ

2

2

4

16

Методи статичного аналізу ПЗ

2

2

4

17

Формальні методи верифікації

2

1

4




Модульна контрольна робота













ВСЬОГО

34

17

57

Загальний обсяг годин – 108, у тому числі


Лекцій – 34 год.

Лабораторних робіт – 17 год.

Самостійна робота – 57 год.

ТЕМАТИЧНО-ЗМІСТОВНА ЧАСТИНА КУРСУ


Змістовий модуль 1. Життєвий цикл розробки програмного забезпечення (ПЗ)


Лекція 1. Проблема розробки програмного програмного забезпечення. – 2 год.

Програмний проект та його тріада. Проблема розробка програмних проектів. Основні категорії розробки ПЗ. [1,6].



Завдання для самостійної роботи (2 год.)

Основні питання управління програмними проектами. [1,4]



Лекція 2. Життєвий цикл ПЗ та методології розробки його життєвого циклу . – 2 год.

Поняття життєвого циклу ПЗ. Послідовні та ітераційні методології розробки ПЗ [1,4,6].



Лабораторна робота 1. (2 год.)

Ознайомлення з засобами розробки програм в середовищі MS Visual Studio та методологією розробки MSF (Microsoft Solutions Framework) [7].

Завдання для самостійної роботи (3 год.)

Вивчення особливостей та порівняльна характеристика різних методологій розробки програм (MSF,RUP,XP) [1, 4, 6].



Змістовий модуль 2. Методи перевірки правильності та тестування програм

Лекція 3. Інженерія вимог до ПЗ – 2 год.

Структура специфікації вимог згідно міжнародних стандартів щодо ПЗ [1,6].



Завдання для самостійної роботи (4 год.)

Вивчення різних підходів до моделювання вимог (моделі станів, зміни станів та поведінки) [1,4].



Лекція 4. Поняття верифікації і валідації програмного забезпечення – 2 год.

Місце верифікації серед процесів розробки програмного забезпечення. Завдання верифікації та валідації ПЗ [1,3,6].



Лабораторна робота 2. (2 год.)

Сценарний підхід до розробки вимог [1,6].



Завдання для самостійної роботи (4 год.)

Вивчення проблеми забезпечення якості ПЗ та основних положень міжнародних стандартів щодо якості програмного забезпечення. [1,2,6].

Лекція 5. Класифікація відмов та помилок у ПЗ. – 2 год.

Класифікація помилок ПЗ: помилки, дефекти та відмови. [1].



Завдання для самостійної роботи (2 год.)

Категорії дефектів розробки програм. Причини появи помилок на етапах ЖЦ [1,3]



Лекція 6. Основні поняття та методи тестування програм [1] – 2 год.

Завдання для самостійної роботи (4 год.)

Вивчення статичних та динамічних методів тестування програм [3].

Лекція 7. Процеси тестування програмних систем - (2 год.)

Класифікація тестів перевірки за об'єктами тестування на основних стадіях розробки. [3]



Лабораторна робота 3. (2 год.)

Розробка планів тестування ПЗ та його проведення. [3]



Завдання для самостійної роботи (2 год.)

Засоби автоматизації процесу тестування [3].

Змістовий модуль 3. Методи доведення правильності програм

Лекція 8. Формальне моделювання програмних систем - (2 год.)

Засоби специфікації програм. Формальне моделювання програмних систем [2].

Завдання для самостійної роботи (4 год.)

Методи створення моделі першого порядку з тексту програми [2].



Лекція 9. Методи доведення правильності програм - (2 год.)

Метод індуктивних тверджень Флойда-Наура та метод структурної індукції Хоара. [1]



Лабораторна робота 4. (2 год.)

Техніки формального доведення правильності програм. . [1]



Завдання для самостійної роботи (4 год.)

Метод Дейкстри формального доведення правильності програм [1].

Лекція 10. Логічні засоби специфікацій програм - (2 год.)

Темпоральні логіки, логіка дерев обчислень CTL* [2].


Завдання для самостійної роботи (4 год.)

Повнота операторів логіка дерев обчислень CTL* [2].

Лекція 11. Перевірка формул на моделі - (2 год.)

Верифікація моделей для логіки дерев обчислень CTL. [2].

Лабораторна робота 5. (2 год.)

Верифікація моделі ПЗ пристрою (мікрохвильова піч) [2].



Завдання для самостійної роботи (2 год.)

Алгоритми верифікації моделей для логіка дерев обчислень CTL [2].

Лекція 12. Двійкові діаграми рішень - (2 год.)

Ефективне подання булевих функцій та метод двійкових діаграм рішень [2].



Завдання для самостійної роботи (4 год.)

Подання моделей Кріпке засобами двійкових діаграм [2].

Лекція 13. Символьна верифікація моделей - (2 год.)

Алгоритми верифікаціъ моделей для логіки LTL [2].



Лабораторна робота 6. (2 год.)

Символьна верифікація на моделі ПЗ пристрою (мікрохвильова піч) [2].



Завдання для самостійної роботи (2 год.)

Символьна верифікація моделей для LTL [2].

Лекція 14. Процеси верифікації ПЗ - (2 год.)

Процеси, артефакти та стандарти верифікації ПЗ [3].



Завдання для самостійної роботи (4 год.)

Завдання верифікації в ЖЦ ПЗ. Верифікація і валідація ПЗ [3].

Лекція 15. Інспекційні методи верифікації ПЗ - (2 год.)

Класифікація методів верифікації. Експертизи ПЗ. [1,3]



Лабораторна робота 7 (2 год.)

Застосування інспекційного методу верифікації ПЗ. [1,3]



Завдання для самостійної роботи (4 год.)

Практика застосування експертиз ПЗ [3].



Лекція 16. Методи статичного аналізу ПЗ - (2 год.)

Статичний аналіз властивостей артефактів. [3]



Лабораторна робота 8 (2 год.)

Застосування статичного аналізу програм[1,3]



Завдання для самостійної роботи (4 год.)

Динамічні методи верифікації ПЗ [3]



Лекція 17. Формальні методи верифікації - (2 год.)

Логіко-алгебричні та виконувані моделі верифікації ПЗ [2,3]



Лабораторна робота 9 (1 год.)

Застосування логіко-алгебричного методу до верифікації ПЗ. [2,3]



Завдання для самостійної роботи (4 год.)

Синтетичні методи верифікації ПЗ [3].


Перелік лабораторних робіт

  1. Методології розробки програмного забезпечення: MSF, RUP та XP.

  2. Ознайомлення з засобами розробки програм в середовищі MS Visual Studio та методологією розробки MSF (Microsoft Solutions Framework)

  3. Методи збирання, аналізу та розробки вимог до ПЗ

  4. Сценарний підхід до розробки вимог

  5. Практичне визначення виду помилок у середовищі MS Visual Studio

  6. Реалізація функціонального тестування в середовищі MS Visual Studio.

  7. Розробка планів тестування ПЗ та його проведення.

  8. Моделювання станів програми за допомогою моделей Кріпке

  9. Техніки формального доведення правильності програм

  10. Специфікація поведінки програм засобами темпоральної логіки

  11. Верифікація моделі ПЗ пристрою (мікрохвильова піч)

  12. Канонічне подання булевих функцій

  13. Символьна верифікація на моделі ПЗ пристрою (мікрохвильова піч)

  14. Верифікація різних артефактів життєвого циклу ПЗ

  15. Застосування інспекційного методу верифікації ПЗ.

  16. Застосування статичного аналізу програм

  17. Застосування логіко-алгебричного методу до верифікації ПЗ.


Теми до проведення колоквіумів

  1. Основні етапи та стратегії розробки програмного забезпечення.

  2. Верифікація та валідації програмних систем.

  3. Основи техніки тестування програм

Питання до іспиту

  1. Програмний проект та його тріада

  2. Проблема розробка програмних проектів.

  3. Основні категорії розробки ПЗ.

  4. Методології розробки програмного забезпечення MSF

  5. Методології розробки програмного забезпечення RUP

  6. Методології розробки програмного забезпечення XP

  7. Поняття життєвого циклу ПЗ. Послідовні та ітераційні методології розробки

  8. Методи збирання та аналізу вимог до ПЗ

  9. Розробка вимог до ПЗ

  10. Специфікація вимог до ПЗ

  11. Сценарний підхід до розробки вимог

  12. Завдання верифікації та валідації ПЗ

  13. Класифікація відмов та помилок у ПЗ

  14. Причини появи помилок на етапах ЖЦ

  15. Основні поняття та методи тестування програм

  16. Процеси тестування програмних систем

  17. Засоби автоматизації процесу тестування в середовищі MS Visual Studio

  18. Засоби формальної специфікації програм

  19. Моделювання станів програми за допомогою моделей Кріпке

  20. Методи створення моделі першого порядку з тексту програми

  21. Методи доведення правильності програм

  22. Логічні засоби специфікацій програм

  23. Специфікація поведінки програм засобами темпоральної логіки

  24. Перевірка формул на моделі

  25. Метод двійкових діаграм рішень для подання булевих функцій

  26. Подання моделей Кріпке засобами двійкових діаграм

  27. Символьна верифікація моделей

  28. Процеси верифікації ПЗ

  29. Верифікація різних артефактів життєвого циклу ПЗ

  30. Інспекційні методи верифікації ПЗ

  31. Методи статичного аналізу ПЗ

  32. Динамічні методи верифікації ПЗ

  33. Формальні методи верифікації

  34. Синтетичні методи верифікації ПЗ

Рекомендована література

Основна

  • 1. Л.П. Бабенко, К.М. Лавріщева. Основи програмної інженерії. К.:”Знання”, 2001.- 269 с.

  • 2. Э. М. Кларк, О. Грамберг, Д. Пелед, Верификация моделей программ: Model Checking. Пер. с англ. под ред. Р. Смелянского.-- Издательство Московского центра непрерывного математического образования, Москва 2002, 416 с.

  • 3. С.В. Синицын, Н.Ю. Налютин, Верификация программного обеспечения, Интернет-Университет Информационных Технологий,  www.INTUIT.ru

Додаткова

  • 4. М. Кантор, Управление программными проектами. - М,: ИД «Вильямс», 2002.- 176 с.

  • 5. И. Соммервилл, Инженерия программного обеспечения. М,: ИД «Вильямс», 2002.- 624 с.

  • 6. С.А. Орлов, Технологии разработки программного обеспечения.- СПб: «Питер», 2002.- 464.

  • 7. Microsoft Visual Studio 2005-2008, www.microsoft.com .


База даних захищена авторським правом ©lecture.in.ua 2016
звернутися до адміністрації

    Головна сторінка