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

    Belépés
    címtáras azonosítással
    vissza a tantárgylistához   nyomtatható verzió    

    Formális módszerek

    A tantárgy angol neve: Formal Methods

    Adatlap utolsó módosítása: 2026. január 9.

    Budapesti Műszaki és Gazdaságtudományi Egyetem
    Villamosmérnöki és Informatikai Kar     		Mérnökinformatikus mesterképzés (MSc)
    Tantárgykód Szemeszter Követelmények Kredit Tantárgyfélév
    VIMIMA26   3/0/0/f 5  
    3. A tantárgyfelelős személy és tanszék Dr. Majzik István,
    A tantárgy tanszéki weboldala http://www.mit.bme.hu/oktatas/targyak/VIMIMA26
    4. A tantárgy előadója Dr. Majzik István docens, MIT
    5. A tantárgy az alábbi témakörök ismeretére épít Programozás alapjai, digitális technika
    6. Előtanulmányi rend
    Kötelező:
    NEM
    (TárgyEredmény( "BMEVIMIMA07", "jegy" , _ ) >= 2
    VAGY
    TárgyEredmény("BMEVIMIMA07", "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 a 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 legfontosabb modellezési nyelveket, valamint a kapcsolódó analitikus és szimulációs vizsgálati módszereket. 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.
    8. A tantárgy részletes tematikája
    1. A formális módszerek szerepe az informatikai rendszerek fejlesztésében (bevezető): formális követelmény-specifikáció, modellezés, verifikáció (modellellenőrzés, helyességbizonyítás) szerepe. Mérnöki és formális modellek kapcsolata, modell-leképzések. Formális módszereket alkalmazó tervezőrendszerek (példák).
    2. Alapszintű formális modellek és szemantikájuk: Kripke struktúrák, tranzíciós rendszerek, Kripke tranzíciós rendszerek, időzített automaták és időzített automaták hálózata.
    3. Követelmények formalizálása temporális logikákkal: Lineáris temporális logika (LTL), elágazó idejű temporális logikák (CTL, CTL*). A kifejezőképesség összehasonlítása.
    4. Formális verifikáció modellellenőrzéssel: Modellellenőrzés tabló módszerrel, valamint szimbolikus technikákkal. Időfüggő viselkedés ellenőrzése.
      Kijelölt írásos tananyag: Tutorial on UPPAAL. https://uppaal.org/documentation/
    5. Nagyméretű állapottérrel rendelkező modellek verifikációja: Az állapottér kezelése döntési diagramok használatával. Korlátos modellellenőrzés.
    6. Gyakorlati alkalmazások: Beágyazott vezérlők és protokollok modellezése időzített automatákkal, temporális követelmények ellenőrzése az UPPAAL modellellenőrző használatával. Automatikus tesztgenerálás modellellenőrzővel. Monitor szintézis temporális logikai követelmények alapján.
    7. Állapotfüggő viselkedés magas szintű modellezése: Állapottérképek formális szemantikája. Tervezés állapottérképek használatával, az állapottérképek verifikációja. Az állapottérkép alapú forráskód szintézis elterjedt megoldásai.
    8. Konkurens rendszerek modellezése és viselkedési tulajdonságainak vizsgálata: A Petri háló formalizmus. Modellek dinamikus tulajdonságainak (holtpontmentesség, élőség, korlátosság, perzisztencia, visszatérő állapotok) ellenőrzése szimulációval és az elérhetőségi gráf alapján. Hierarchikus Petri hálók. Modellezési mintapéldák.
    9. Konkurens rendszerek strukturális tulajdonságainak vizsgálata: Állapotokra és viselkedésre vonatkozó invariánsok, strukturális korlátosság és vezérelhetőség kifejezése és ellenőrzése. Tulajdonságmegőrző modell-redukciós technikák.
    10. Adatfüggő viselkedés modellezése: Adattípusok és adatkezelés modellezése. A dinamikus és strukturális tulajdonságok kiterjesztése. Gyakorlati alkalmazások: Elosztott adatkezelés konzisztenciájának vizsgálata, protokollok analízise.
    11. 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 analízishez, teljesítmény és megbízhatósági tulajdonságok vizsgálata.
    12. Modellfinomítás: A szisztematikus modellfinomítás módszerei. A modellfinomítás konzisztenciájának ellenőrzése a viselkedésre vonatkozó relációk használatával.
    13. 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.
    14. Program helyességbizonyítás: Kontraktusok, elő- és utófeltételek, invariánsok formalizálása, ellenőrzésük az algoritmusok magas szintű leírása illetve köztes reprezentációja alapján.
    9. A tantárgy oktatásának módja (előadás, gyakorlat, laboratórium) Előadás.
    10. Követelmények

    A félévközi jegy megszerzésének követelménye két zárthelyi legalább elégséges szintű teljesítése. Sikeres zárthelyik jegye egy-egy jeggyel javítható opcionális modellezési és verifikációs (otthoni) feladatok megoldásával. A félévközi jegyet 50%-50%-os súllyal a két zárthelyi osztályzata határozza meg.

    11. Pótlási lehetőségek A szorgalmi időszak során minden zárthelyi dolgozathoz tartozik egy pótzárthelyi alkalom. Ez felhasználható az elmulasztott vagy sikertelen zárthelyi pótlására, vagy a sikeres zárthelyi eredményének javítására. A pótzárthelyi eredménye felülírja a korábbi eredményt - akkor is, ha az rosszabb, mint a korábbi.
    12. Konzultációs lehetőségek Az opcionális otthoni feladatok megoldásához konzultáció biztosított.
    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.
    • Bartha Tamás, Majzik István: Biztonságra tervezés és biztonságigazolás formális módszerei. Akadémiai Kiadó, 2019.
    • E. M. Clarke, O. Grumberg, D. Kroening, D. Peled, H. Veith: Model Checking. 2nd edition, MIT Press, 2018. ISBN 9780262038836
    14. A tantárgy elvégzéséhez átlagosan szükséges tanulmányi munka
    Kontakt óra42
    Félévközi készülés órákra28
    Felkészülés zárthelyire68
    Házi feladat elkészítése0
    Kijelölt írásos tananyag elsajátítása12
    Vizsgafelkészülés0
    Összesen150
    15. A tantárgy tematikáját kidolgozta Dr. Majzik István docens, MIT
    Dr. Pataricza András egyetemi tanár, MIT
    Egyéb megjegyzések A tantárgy angol neve: Formal Methods.