Формальнi методи розробки програмних систем

Освітня програма: Штучний інтелект

Структурний підрозділ: Факультет комп'ютерних наук та кібернетики

Назва дисципліни
Формальнi методи розробки програмних систем
Код дисципліни
ННД.07
Тип модуля
Обов’язкова дисципліна для ОП
Цикл вищої освіти
Другий
Рік навчання
2023/2024
Семестр / Триместр
2 Семестр
Кількість кредитів ЕСТS
4
Результати навчання
ПРН1. Мати спеціалізовані концептуальні знання, що включають сучасні наукові здобутки у сфері комп'ютерних наук і є основою для оригінального мислення та проведення досліджень, критичне осмислення проблем у сфері комп’ютерних наук та на межі галузей знань. ПРН2. Мати спеціалізовані уміння/навички розв’язання проблем комп’ютерних наук, необхідні для проведення досліджень та/або провадження інноваційної діяльності з метою розвитку нових знань та процедур. ПРН4. Управляти робочими процесами у сфері інформаційних технологій, які є складними, непередбачуваними та потребують нових стратегічних підходів. ПРН6. Розробляти концептуальну модель інформаційної або комп’ютерної системи. ПРН7. Розробляти та застосовувати математичні методи для аналізу інформаційних моделей. ПРН13. Оцінювати та забезпечувати якість інформаційних та комп’ютерних систем різного призначення. ПРН16. Виконувати дослідження у сфері комп’ютерних наук.
Форма навчання
Дистанційне навчання
Попередні умови та додаткові вимоги
Знати: основні поняття, засоби і методи математичної логіки, їх застосування в інформатиці й програмуванні; знати мови пропозиційної логіки та логіки 1-го порядку, їх можливості для опису предметних областей; основні методи пошуку доведень та засоби логічного виведення. Вміти: описувати на формальних мовах 1-го порядку твердження для різних предметних областей; встановлювати істинність пропозиційних формул, безкванторних формул, формул 1-го порядку; встановлювати наявність логічного наслідку; встановлювати виразність та невиразність предикатів у моделях мови. Володіти елементарними навичками: програмування в сучасних мовах, перевірки виконуваності формул.
Зміст навчальної дисципліни
Мета дисципліни – засвоєння основних концепцій, принципів, методів та інструментів розробки програмних систем з використанням формальних підходів для створення сучасних програмних високої якості. Навчальна дисципліна "Формальні методи розробки програмних" є складовою освітньо-наукової програми підготовки спеціалістів за освітньо-кваліфікаційним рівнем «магістр» галузі 12 "Інформаційні технології" зі спеціальності 122 «Комп’ютерні науки», освітньо-наукової програми "Інформатика". Дана дисципліна є обов’язковою навчальною дисципліною за програмою "Інформатика". Викладається в 2 семестрі 1 курсу магістратури в обсязі 120 годин (4 кредити ECTS), зокрема: лекції – 30 год., семінари – 8 год., консультації – 2 год., самостійна робота – 80 год. У курсі передбачено 2 частини та 2 контрольні роботи. Завершується дисципліна іспитом у 2-му семестрі.
Рекомендована та необхідна література
1. Roggenbach M., Cerone A., Schlingloff B.-H., Schneider G, Shaikh S.A. Formal Methods for Software Engineering Languages, Methods, Application Domains. Springer, 2022, 524 p. 2. Nielson F., Nielson H.R. Formal methods. An appetizer. Springer, 2019, 160 p. 3. Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, 2002 Pearson Education Publ. 4. Steve Schneider. The B-Method: An Introduction, Cornerstones of Computing series, 2001. ISBN 0-333-79284-X. 5. Schneider K.: Verification of Reactive Systems. Formal Methods and Algorithms. Springer-Verlag Berlin Heidelberg (2004). 6. Jim Davies and Jim Woodcock. Using Z: Specification, Refinement and Proof. Prentice Hall International Series in Computer Science, 1996. 7. Dafny Online Tutorial. URL: https://dafny.org/dafny/OnlineTutorial/guide.html 8. The RAISE specification language. Prentice Hall Int.– 1992.– 397 p.
Заплановані освітні заходи та методи викладання
Лекція, самостійна робота, захист проєкту.
Методи та критерії оцінювання
Семестрове оцінювання: 1. Контрольна робота 1 / РН 1.1., РН 1.2 — 25 балів/15 балів. 2. Контрольна робота 2 / РН1.3 – 25 балів/15 балів. 3. Захист проекту / РН2.1, РН3.1, РН4.1 – 10 балів/6 балів Підсумкове оцінювання (у формі іспиту) - максимальна кількість балів: 40; - результати навчання які будуть оцінюватись: PH1.1, PH1.2, PH1.3, PH2.1, РН3.1, РН4.1; - форма проведення і види завдань: письмова Критерії оцінювання відповіді студента на питання: - повнота розкриття питання 1-4 бали; - логіка викладення 2 бал; - аналітичні міркування 1-4 бали.
Мова викладання
Українська, англійська

Кафедри

Наступні кафедри задіяні у викладанні наведеної дисципліни

Теорії та технології програмування
Факультет комп'ютерних наук та кібернетики