Formális módszerek

Tárgyfelelős

A munkatárs fényképe
tanszékvezető helyettes, habilitált docens
Szoba: IB421
Tel.:
+36 1 463-3598
Email: majzik (*) mit * bme * hu

Oktatók

A munkatárs fényképe
tanszékvezető helyettes, habilitált docens
Szoba: IB421
Tel.:
+36 1 463-3598
Email: majzik (*) mit * bme * hu

Hirdetmények

Tartalomátvétel

Bevezetés

Az informatikai rendszerek bonyolultságának és a potenciális hibák kockázatának növekedésével mindinkább elvárás az, hogy a kritikus funkciók tervezése és megvalósítása bizonyítottan helyes (hibamentes) legyen. Ennek egyik jellegzetes megoldása a formális módszereket alkalmazó fejlesztés: formális modellek biztosítják a követelmények és tervek egyértelmű és precíz rögzítését, formális verifikációval vizsgálhatók a tervezői döntések és bizonyíthatók a tervek egyes tulajdonságai, az ellenőrzött tervek pedig alapját képezhetik az automatikus forráskód szintézisnek. A tárgy áttekintést ad az informatikai rendszerek formális modelljeinek megalkotásához és analíziséhez szükséges számításelméleti háttérről, ideértve a tervek és követelmények leírására szolgáló legfontosabb formalizmusokat, valamint a kapcsolódó verifikációs és validációs technikákat. A tárgy demonstrálja a formális módszerek alkalmazását a követelmény-specifikáció, a rendszer- és szoftvertervezés, a modell alapú verifikáció, valamint a forráskód szintézis területén. A tantárgy követelményeit eredményesen teljesítő hallgatók (1) megismernek és alkalmazni tudnak különböző formális módszereket, (2) képesek lesznek nem-formális rendszerleírások alapján formális modellt alkotni, (3) tisztában lesznek a formális verifikációs technikák előnyeivel és korlátaival, (4) megismernek formális módszereket támogató alapvető eszközöket.