Formális módszerek

A tantárgy angol neve: Formal Methods

Adatlap utolsó módosítása: 2018. február 22.

Budapesti Műszaki és Gazdaságtudományi Egyetem
Villamosmérnöki és Informatikai Kar

Mérnök informatikus szak, MSc képzés
Elágazó közös tantárgy 

Tantárgykód Szemeszter Követelmények Kredit Tantárgyfélév
VIMIMA07 1, 2 3/0/0/f 4  
3. A tantárgyfelelős személy és tanszék Dr. Majzik István,
A tantárgy tanszéki weboldala https://www.mit.bme.hu/oktatas/targyak/vimima07
4. A tantárgy előadója Dr. Majzik István, egyetemi docens, MIT
6. Előtanulmányi rend
Kötelező:
NEM ( TárgyEredmény( "BMEVIMIM100" , "jegy" , _ ) >= 2
VAGY
TárgyEredmény("BMEVIMIM100", "FELVETEL", AktualisFelev()) > 0
VAGY
TárgyEredmény( "BMEVIMIMA26" , "jegy" , _ ) >= 2
VAGY
TárgyEredmény("BMEVIMIMA26", "FELVETEL", AktualisFelev()) > 0)

A fenti forma a Neptun sajátja, ezen technikai okokból nem változtattunk.

A kötelező előtanulmányi rend az adott szak honlapján és képzési programjában található.

7. A tantárgy célkitűzése
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.
8. A tantárgy részletes tematikája
 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.

9. A tantárgy oktatásának módja (előadás, gyakorlat, laboratórium) Előadás.
10. Követelmények
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: -

11. Pótlási lehetőségek Bármelyik zárthelyi egyszeri pótlására van lehetőség. Házi feladatok határidőn túl a pótlási időszakban adhatók be, a késedelmes beadás 20% pontlevonással jár.
12. Konzultációs lehetőségek A házi feladattal kapcsolatban a félév során konzultációs lehetőséget biztosítunk.
13. Jegyzet, tankönyv, felhasználható irodalom
 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
Ajánlott irodalom:
 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.

14. A tantárgy elvégzéséhez átlagosan szükséges tanulmányi munka
Kontaktóra
42
Készülés előadásra
12
Önálló tananyag-feldolgozás
12
Nagyzárthelyi

32

Házi feladat
22
Összesen120
15. A tantárgy tematikáját kidolgozta
 Dr. Majzik István, egyetemi docens, MIT
 Dr. Bartha Tamás, egyetemi docens, MIT
 Dr. Pataricza András, egyetemi tanár, MIT

Egyéb megjegyzések A tantárgy neve angolul: Formal Methods