Formális módszerek
Tárgyfelelős:
Majzik István
Tárgy adatlap:
https://portal.vik.bme.hu/kepzes/targyak/VIMIMA07/
Aktuális információk a 2020/21 tanév tavaszi félévére
- 2021-től az aktuális információk a kari Moodle rendszerben találhatók.
- Lentebb archivált információk olvashatók a 2020-as évből.
Archivált információk: VIK Mérnökinformatikus szak, 2020 tavasz
- Hirdetmény a távoktatásról
- Tudnivalók a tárgyról
- Diasorok, segédanyagok
- Zárthelyi információk
- Házi feladat információk
- Szorgalmi feladat információk
- Záróvizsga kérdések
- Közzétett hírek
Archivált információk: VIK Mérnökinformatikus szak, angol képzés, 2020 tavasz
Archivált információk: GTK Mérnöktanári szak, levelező képzés, 2020 tavasz
Hirdetmény a VIK hallgatóinak a 2020. március 23-tól kezdődő távoktatásról
-
A tárgy előadásait online technikákkal fogjuk megtartani az eredeti órarendi ütemezésnek megfelelően: minden szerda 14:15-17:00.
- Csatlakozni közvetlenül az MS Teams alkalmazásban lehet (regisztrációs részleteket ld. lentebb).
- Az MS Teams hasznnálatához kérünk mindenkit, hogy hozzon létre eduID azonosítót és Office365 hozzáférést a VIK Távoktatás tájékoztatójában leírtak szerint.
- A Teams belépés után a „Formális módszerek - VIMIMA07HU” csoportban jelennek meg az előadások meghívói. Aki nem tud a csoporthoz csatlakozni, kérem, hogy jelezze ezt a tárgyfelelősnek (majzik@mit.bme.hu).
- Az előadás megosztott és hangalámondással kísért diasorok segítségével történik. Az előadás előtt (a Teams-hez való hozzáférés mellett) más felkészülés nem szükséges. Jelenléti ellenőrzés nem lesz.
- Az előadáson bemutatott diasorok offline tanuláshoz rendelkezésre állnak majd a szokásos módon a tárgy Segédanyagok oldalán. Egyes témákhoz ezen kívül jegyzet részleteket is fogunk kiadni.
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.
