×
Универзитет у Новом Саду

Предмет: Формалне методе у моделовању софтверских система (17.IFE256)

Матичне организационе јединице предмета: Катедра за примењене рачунарске науке

Основне информације:
 
Категорија Научно-стручни
Ужа научна област Примењене рачунарске науке и информатика
ЕСПБ 6

Образовање студената у области формалних метода у моделовању софтверских система и система у којима се примењује софтвер. Овладавање приступима и техникама примене формалних метода у моделовању софтверских система и система у којима се примењује софтвер.

По завршетку курса студенти ће бити оспособљени да: • Користе математичке концепте типа скупа, скупа са дупликатима, функције и релације, у циљу формалне спецификације софтверских система и њихових карактеристика. • Врше проверу формалних спецификација, проверу модела и доказују задовољење захтеваних особина софтверских система. • Користе математичко размишљање за доказивање задовољења особина софтверских модела. • Креирају спецификације трансформација модела, односно генераторе програмског кода из спецификација, и у једноставнијим случајевима изврше формалну проверу генерисаног кода.

Увод у формалне методе. З нотација. Хоареова логика и верификација програма. Хоареове тројке. Делимична и потпуна коректност. Доказивање делимичне коректности. Најслабији предуслови и аутоматска верификација. Примена темпоралне логике и других врста логика у моделовању система и провери модела. Темпорална логика у линеарном времену (ТЛЛВ). Провера модела применом приступа заснованог на теорији аутомата. Провера модела заснована на примени ТЛЛВ.

Настава се изводи у облику предавања, аудиторних и рачунарских вежби (у рачунарској лабораторији) и консултација. Током целокупног процеса извођења наставе, студенти се подстичу на интензивну комуникацију, критичко резоновање, самостални рад и активан однос према процесу наставе. Услов за добијање потписа и излазак на завршни испит представља извршење свих предиспитних обавеза, у минималном обиму од 30 поена.

Аутори Назив Година Издавач Језик
Michael Huth, Mark Ryan Logic in Computer Science: Modelling and Reasoning about Systems 2004 Cambridge University Press Енглески
J. M. Spivey The Z Notation: A Reference Manual 1992 Prentice Hall Енглески
R. D. Tennent Specifying Software: A Hands-On Introduction 2002 Cambridge University Press Енглески
Предметна активност Предиспитна Обавезна Број поена
Предметна активност
Предметни пројекат
Предиспитна
Да
Обавезна
Да
Број поена
30.00
Предметна активност
Тест
Предиспитна
Да
Обавезна
Да
Број поена
10.00
Предметна активност
Сложени облици вежби
Предиспитна
Да
Обавезна
Да
Број поена
20.00
Предметна активност
Тест
Предиспитна
Да
Обавезна
Да
Број поена
10.00
Предметна активност
Усмени део испита
Предиспитна
Не
Обавезна
Да
Број поена
30.00
API Image

ванр. проф. др Душан Гајић

Ванредни професор

Предавања

Предавања

Рачунарске вежбе

Рачунарске вежбе