Formális módszerek

Senior Lecturer: 
István Majzik
Instructors: 
Dániel Darvas
Instructors: 
Rebeka Farkas
Instructors: 
István Majzik
Instructors: 
Tamás Tóth
Instructors: 
András Vörös

 

Aktuális információk: VIK Mérnökinformatikus szak, 2017 tavasz

Aktuális információk: VIK Mérnökinformatikus szak, angol képzés, 2017 tavasz

Aktuális információk: GTK Mérnöktanári szak, levelező képzés, 2017 tavasz

A tá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 követelmény az, hogy a kritikus komponensek megvalósítása bizonyítottan helyes legyen. Ennek egyik jellegzetes megoldása a formális modelleken alapuló tervezés és megvalósítás: A formális modellek analízisével vizsgálhatóvá válnak a tervezői döntések, bizonyíthatóak egyes tulajdonságok, valamint automatizálható a kódszintézis. 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. Demonstrálja ezek alkalmazását a rendszerszintű modellezés, a hardver tervezés, valamint a szoftver helyességbizonyítás és szintézis területén.

A tantárgy követelményeit eredményesen teljesítő hallgatók

  • ismernek és alkalmazni tudnak különböző formális módszereket és technológiákat,
  • képesek nem-formális rendszerleírások alapján formális modellt alkotni,
  • ismerik a különböző helyességbizonyítási technikák előnyeit és hátrányait,
  • tisztában vannak a formális módszereket támogató alapvető eszközökkel.

A tá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. 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).
  • Á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.