РЕГРЕСИОНА ВЕРИФИКАЦИЈА СОФТВЕРА КОРИШЋЕЊЕМ СИСТЕМА LAV

Milena Vujošević Janičić

Milena Vujošević Janičić Matematički fakultet, Univerzitet u Beogradu

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

Сажетак

Алати за аутоматску верификациjу софтвера постигли су огроман напредак и постаjу све шире практично употребљиви. Oднедавно се практично разматра и jедан нови вид верификациjе софтвера — регресиона верификациjа. У регресионоj верификациjи, слично као у регресионом тестирању, функционална исправност програма проверава се тако што се испитуjе еквивалентност са програмом за коjи се претпоставља да jе исправан. Наравно, регресиона верификациjа, онда када jе применљива, даjе много поузданиjе и дубље закључке него регресионо тестирање. У овом раду описаћемо укратко основне поjмове верификациjе софтвера и показати да верификациjски систем LAV може успешно да се користи за регресиону верификациjу. Могуће примене су у развоjу софтвера (као алтернатива регресионом тестирању) али и у образовању, за аутоматску евалуациjу студентских програма.