Budapest University of Technology and Economics, Faculty of Electrical Engineering and Informatics

Kötelező:

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
- megismernek és alkalmazni tudnak különböző formális módszereket,
- képesek lesznek nem-formális rendszerleírások alapján formális modellt alkotni,
- tisztában lesznek a formális verifikációs technikák előnyeivel és korlátaival,
- megismernek formális módszereket támogató alapvető eszközöket.

 Informatikai rendszerek formális modellezése és analízise (a tantárgy bevezetése): A formális módszerek szerepe az informatikai rendszerek fejlesztésében: formális követelmény-specifikáció, modellezés, verifikáció (modellellenőrzés, helyességbizonyítás). Mérnöki és formális modellek kapcsolata, modell-transzformációk. Formális módszereket alkalmazó tervezőrendszerek (pl. SCADE).

 Alapszintű formális modellek és szemantikájuk: Kripke-struktúrák, tranzíciós rendszerek, időzített automaták, időzített automaták hálózata.

 Követelmények formalizálása: Temporális logikák: lineáris temporális logika (LTL), elágazó idejű temporális logikák (CTL, CTL*). A kifejezőképesség összehasonlítása. Gyakorlati példák és alkalmazások (Property Specification Language).

 Formális verifikáció modellellenőrzéssel: Modellellenőrzés tabló módszerrel, valamint szimbolikus technikákkal. Az állapottér kezelése bináris döntési diagramok használatával. Korlátos modellellenőrzés. Időfüggő viselkedés verifikációja.  Gyakorlati alkalmazások: Beágyazott vezérlők modellezése időzített automatákkal, temporális követelmények ellenőrzése, automatikus tesztgenerálás modellellenőrzővel. Az UPPAAL modellellenőrző (kijelölt tananyag alapján).

 Állapotfüggő dinamikus viselkedés modellezése: Állapottérképek formális szintaktikája és szemantikája. Tervezés állapottérképek használatával, az állapottérképek formális verifikációja. A forráskód szintézis elterjedt mintái. Gyakorlati alkalmazások: UML 2 állapottérképek, szoftver forráskód generálás és monitor szintézis a gyakorlatban.

 Konkurens rendszerek modellezése és analízise: A Petri háló formalizmus. Modellek dinamikus tulajdonságai (biztonságosság, élőség, korlátosság, visszatérő állapotok), ezek ellenőrzése szimulációval és az elérhetőségi gráf alapján. Strukturális tulajdonságok (konzervativitás és konzisztencia kifejezése invariánsokkal) és vizsgálatuk az állapotegyenlet alapján. Tulajdonságmegőrző modell-redukciós technikák. Hierarchikus Petri hálók. Modellezési mintapéldák.

 Adatfüggő viselkedés modellezése: A Petri hálók bővítése adattípusokkal és adatkezeléssel. A dinamikus és strukturális tulajdonságok kiterjesztése. Gyakorlati alkalmazások: Elosztott adatkezelés konzisztenciájának vizsgálata, protokoll analízis.

 Extra-funkcionális tulajdonságok specifikálása és verifikációja: A Petri hálók kiterjesztése valószínűségi és idő jellemzőkkel: sztochasztikus Petri hálók. Követelmények formalizálása sztochasztikus temporális logikákkal. Teljesítmény és megbízhatósági tulajdonságok analízise.

 Adatfeldolgozás modellezése: Adatfolyam hálók szintaktikája és szemantikája. Modellfinomítás, a finomítás konzisztenciájának ellenőrzése. Adatfolyam hálók alkalmazása üzleti folyamatok modellezésére és hibaterjedési vizsgálatokra.

 Szoftver forráskód alapú formális verifikációs technikák: Modellellenőrzés C programokon. Absztrakció használata: statikus analízis absztrakt interpretációval, predikátum absztrakció, ellenpélda vezérelt absztrakció finomítás a modellellenőrzés során.

A szorgalmi időszakban: A félévközi jegy megszerzésének követelménye két zárthelyi és egy házi feladat legalább elégséges szintű teljesítése. A házi feladat részei egy kisméretű informatikai rendszer modelljének elkészítése valamint az elvárt tulajdonságok modell alapú verifikációja. Ehhez kijelölt tananyag alapján önállóan meg kell ismerni a modellező nyelv és eszközkészlet specialitásait. A házi feladat kiadására a 4. oktatási héten kerül sor, a beadásához kapcsolódó bemutatók a 10. oktatási héttől ütemezhetők. A félévközi jegyet 35-35%-os súllyal a két zárthelyi osztályzata és 30%-os súllyal a házi feladat osztályzata határozza meg.

A vizsgaidőszakban: -

 Pataricza András (szerk.): Formális módszerek az informatikában. Második kiadás, TypoTeX Kiadó, 2006.

 G. Behrmann, A. David, K. G. Larsen: A Tutorial on UPPAAL 4.0. http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf

 D. Peled: Software Reliability Methods. Springer Verlag, 2001.

 B. Berard et al.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer Verlag, 2010.

 E. M. Clarke, O. Grumberg, D. Peled:  Model Checking. MIT Press, 1999.

 W. Reisig, G. Rozenberg (eds.): Lectures on Petri Nets. Vol I-II, Springer Verlag, 1998.

 Dr. Majzik István, egyetemi docens, MIT

 Dr. Bartha Tamás, egyetemi docens, MIT

 Dr. Pataricza András, egyetemi tanár, MIT