Інфопакет

Формальні методи програмної інженерії

ВК.1.01

Вибіркова дисципліна для ОП

Другий

2023/2024

3 Семестр

3

РН03. Будувати і досліджувати моделі інформаційних процесів у прикладній області. РН10. Модифікувати існуючі та розробляти нові алгоритмічні рішення детального проєктування програмного забезпечення.

1. Знати певні розділи дискретної математики, насамперед, математичну логіку, теорію алгоритмів, теорію абстрактних автоматів, теорію булевих функцій, теорію графів, теорію алгебраїчних систем та інші. 2. Знати основні поняття програмування та принципи розробки програм.

Мета дисципліни – засвоєння та аналіз основних математичних методів написання специфікацій, розробки та перевірки (англ. verification) програмного забезпечення та комп'ютерного обладнання (на всіх етапах їх життєвого циклу). В результаті вивчення навчальної дисципліни магістрант повинен знати: роль формальних методів в життєвому циклі програм; табличні засоби специфікації програм; рівності, підстановки та проблема визначення семантики; денотаційну, операційну і аксиоматичну семантики, їх зв’язок із підстановками; логічні засоби та аксіоматичні описи; графові засоби специфікації: графи, мережі, діаграми; операції, вирази, процедурні засоби та їх комбінування; засоби модуляризації, типізації, структуризації та їх реалізацію; засоби іменування (зокрема, імена та поняття змінної, контексти та області дії імен); методологічні принципи та прагматичні рекомендації застосування формальних методів програмної інженерії. В результаті вивчення навчальної дисципліни магістрант повинен вміти: застосовувати отримані знання при розробці програмних систем (для яких важливими є надійність або безпека) з метою їх захисту від помилок як на ранніх етапах написання вимог та специфікацій, так і для повністю формальної розробки реалізації програм.

1. Hoare, C.A.R. Communicating Sequential Processes. London: Prentice-Hall International. – 1985. 2. Milner R.G. A Theory of Type Polymorphism in Programming. Journal of Computer and System Science, 1978, 17, p. 348-357. 3. Joseph Goguen and Grant Malcolm, Algebraic Semantics of Imperative Programs. – MIT Press, 1996. 4. Björner, Dines; Henson, Martin C. (Eds.) Logics of Specification Languages, Series: Monographs in Theoretical Computer Science. An EATCS Series 2008, XXII, 624 p. 69 illus., Hardcover. 5. RAISE Method Group. The RAISE Development Method. BCS Practitioner Series. Prentice Hall. 1995. – 493 p. 6. Rod M. Burstall , Joseph A. Goguen, The Semantics of CLEAR, A Specification Language, Proceedings of the Abstract Software Specifications, 1979, Copenhagen Winter School, p. 292-332, January 22-February 02. 7. Guttag J.V., Horning J.J. Larch: Languages and Tools for Formal Specification. – Springer-Verlag, Texts and monographs in Computer Science, 1993. – 259 p.

Лекції, самостійна робота, контрольні роботи, домашні завдання, залік.

Семестрове оцінювання: 1. Контрольна робота 1: СК01, СК04, СК05 - 50 балів / 9 балів. 2. Контрольна робота 2: СК01, СК04, СК05 - 50 балів / 10 балів. Підсумкове оцінювання (у формі диференційованого заліку): 1. Максимальна кількість балів, яка може бути отримана студентом за залік за 100-бальною шкалою: 100 балів; 2. Мінімальний пороговий рівень позитивної оцінки, за якої студент допускається до заліку (за 100-бальною шкалою): 20 балів. 3. Результати навчання, що оцінюються на заліку: СК01, СК04, СК05.

українська