Formális módszerek - GTK levelező képzés (2020 tavasz)

Elérhetőségek

A tárgy web lapjai:

• A tárgy adatlapja a VIK DH oldalán: https://www.vik.bme.hu/kepzes/targyak/VIMIMA19/
• A tárgy részletes web oldala: http://www.inf.mit.bme.hu/edu/courses/form/levelezo

Ajánlott jegyzet:

• Bartha Tamás, Majzik István: Biztonságra tervezés és biztonságigazolás formális módszerei
• Pataricza András (szerkesztő): Formális módszerek az informatikában

Előadások és konzultációk:

• BME I. épület, (helyszín és időpontok megbeszélése folyamatban)

Anyagok a felkészüléshez:

• Előadás diasorok, segédanyagok ezen az oldalon elérhetők (ld. lentebb).

Előadók:

• dr. Majzik István (tárgyfelelős): majzik@mit.bme.hu

Tárgykövetelmények és magyarázatok

• A félévközi jegy megszerzésének követelménye egy zárthelyi és egy házi feladat legalább elégséges szintű teljesítése.
• A félévközi jegyet 70%-os súllyal a zárthelyi osztályzata és 30%-os súllyal a házi feladat osztályzata határozzák meg.
  • A zárthelyire és a házi feladatra is jegyet kap minden hallgató.
  • Mindkét jegyre érvényes, hogy az elégséges szintet el kell érnie.
  • A kapott jegyekből a fenti 70-30% súlyozással alakul ki a félévközi jegy a kerekítés szabályai szerint (*,50-től felfelé kerekítve).
• A sikertelen zárthelyi pótolható.
  • Sikeres zárthelyi javító célzattal történő újraírására is van lehetőség, ez esetben a legutolsó kapott osztályzat lesz érvényes.
• A házi feladat elkészítése kötelező. A házi feladat témája modellezés és modell alapú ellenőrzés.
  • A házi feladat késedelmes leadása a pótlási időszakban lehetséges, a pótbeadás 20% (egy jegy) pontlevonással jár.
  • A házi feladat beadásához bemutató is tartozik, enélkül a beadott házifeladat nem értékelhető. A bemutató során röviden el kell magyarázni a feladat megoldását, és válaszolni kell a feladattal kapcsolatban feltett kérdésekre. Ezek a kérdések elsősorban a megoldásban látott modellezési döntésekre, alternatívákra, az esetleges hibák hátterére vonatkoznak.

A félév időbeosztása

• Konzultációk:
  • 1. konzultáció: 2020. február 19. szerda, 17:15-20:00, I.L.405 terem:
    A formális módszerek szerepe. Formális modellezés.
    Segédanyag: T01-T02. 
  • 2. konzultáció: 2020. március 17. kedd, 10:15-13:00, I.L.405 terem 2020. március 31. 16:30-tól, MS Teams
    Követelmények formalizálása. A modellellenőrzés. Állapottérképek.
    Segédanyag: T03-T06.
  • 3. konzultáció: 2020. április 7. kedd, 17:15-20:00, I.E.224 terem 2020. április 14. 16:30-tól, MS Teams
    Petri-hálók és tulajdonságaik.
    Segédanyag: T07-T08.
  • 4. konzultáció: 2020. május 5. kedd, 17:15-20:00, MS Teams
    Gyakorló feladatok (modellezés) és ellenőrző kérdések megbeszélése.
    Zárthelyi dolgozat megírása. Házi feladat bemutatása.
    Segédanyag: ZH. (Kiegészítő anyag: T09-T11.)
• Zárthelyik:
  • Zárthelyi: A 4. konzultáció során.
  • Pótzárthelyi: A pótlási időszakban, egyénileg egyeztetett időpontban.
• Házi feladat:
  • Házi feladat kiadása: Az 1. konzultációt követően.
  • Házi feladat beadása: A 4. konzultáció előtt egy héttel.
  • A feladatok bemutatása: A 4. konzultáció során.
  • Házi feladat pótbeadása (egy jegy levonással jár): Pótlási hét szerda éjfélig. A vizsgaidőszak 10. napjáig.
  • A pótbeadás bemutatása: Egyénileg egyeztetett időpontban.

Segédanyagok

A zárthelyik

A zárthelyi:

• Időpont: A 4. konzultáció során.
• Témája: A fenti segédanyagok között megtalálható T01 - T08 témák.
• A felkészüléshez használható ellenőrző kérdések és háttéranyagok: A fenti segédanyagok között a ZH anyagai.
• A felkészüléshez használható mintapéldák: A fenti segédanyagok között a ZH anyagai.

A pótzárthelyi:

• Időpont: Egyénileg egyeztetve a pótlási időszakban.
• Témája: A pótolandó zárthelyi témája.

A házi feladat

A tantárgy követelményeinek teljesítéséhez egy otthoni feladatot (a továbbiakban házi feladat) kell kötelezően elkészíteni:

• Az elkészítendő házi feladat kiírása: a fenti segédanyagok között HF jelzéssel.

A házi feladat megoldása során egy szöveges leírással megadott rendszert kell formális modellel leírni, majd a modellen adott követelmények teljesülését (vagy éppen nem teljesülését) igazolni. Célunk, hogy mindenki gyakorlatot szerezzen a formális modellezésben és ellenőrzésben. A modellezés többféleképpen is helyes lehet; a házi feladat elkészítése során azt várjuk el. hogy az informális leírásban foglaltaknak feleljen meg a kidolgozott formális modell.

A házi feladat teljesítésének forgatókönyve az alábbi.

1. A szövegesen megadott rendszernek készítse el a formális modelljét az UPPAAL eszközzel.
   • Röviden dokumentálja a modell felépítését, a modellezési alternatívákat (ha vannak).
   • Indokolja a modell kidolgozása során hozott döntéseket (ha vannak).
   • Szükség esetén finomítsa a kiadott informális leírást.
2. Formalizálja a szöveges leírásban megadott követelményeket az UPPAAL temporális logikai kifejezéseivel.
   • Dokumentálja a formalizált követelményeket.
3. Ellenőrizze a modellen a megadott követelmények teljesülését az UPPAAL verifikációs modulja és a felírt temporális logikai kifejezések segítségével.
   • Írja le a verifikáció kimenetét.
   • Ha egy kritérium igazolása sikertelen, akkor értelmezze az ellenpéldát és lehetőség szerint javítsa ki a hibát.

A házi feladatot önálló munkával kell megoldani. A modellezés fázisában nem tiltott a feladatok szakmai konzultációja egymás közt, de kérjük, hogy alapvetően egyedül dolgozzanak. A dokumentációt mindenkinek önállóan kell elkészítenie. Ezzel demonstrálja, hogy - ha segítettek is neki korábban - megértette és elsajátította a formális modellezés alapvető ismereteit. Másolt dokumentációt tehát nem fogadunk el.

Eszközök a házi feladat kidolgozásához

A modell ellenőrzési feladatot a svédországi Uppsala Egyetem és a dániai Aalborg Egyetem közötti együttműködésben kifejlesztett UPPAAL eszköz segítségével kell megoldani. Az UPPAAL integrált környezetet ad valósidejű rendszerek modellezésére együttműködő időzített automaták segítségével. A működés helyességének vizsgálatát (a modell verifikálását) temporális logikai kifejezések modellellenőrzése révén támogatja. A modelleket az UPPAAL rendszerben bővített adattípusok (egészek, tömbök, stb.) felhasználásával építhetjük fel.

Az UPPAAL felülete Java nyelven íródott. Ez azt is jelenti, hogy Java futtatókörnyezet (pl. J2SE Java Runtime Environment) kell a futtatásához.

Az UPPAAL program aktuális verziója az UPPAAL honlapról regisztrálás után tölthető le. Az oktatási célú felhasználás ingyenes. Ha a telepített hivatalos verzió licensz problémákat jelez, akkor érdemes a fejlesztői verziót használni, vagy legalább egyszer az egyetem (BME) IP címtartományában futtatni.

Az UPPAAL környezet használatának megismerését és a modellezési nyelv elsajátítását az órán elmondottakon túl az alábbi (angol nyelvű) anyagok is segítik:

• UPPAAL bemutató (modellezési példákkal)
• Az UPPAAL dióhéjban
• UPPAAL2K: rövid bemutatás
• Bevezetés az UPPAAL használatába (előadásfóliák) 

Ezen kívül ajánlott az eszközzel együtt adott mintapéldák tanulmányozása, kipróbálása, valamint az eszköz Help menüjéből elérhető leírás átolvasása.

A házi feladat beadása

A követelmények teljesítéséhez a következők beadása szükséges:

• A feladat megoldásának dokumentációja (ábrákkal ellátott szöveges leírás).
  A dokumentáció tartalmazza a modell felépítésének és ellenőrzésének ismertetését, a kapott eredményeket, valamint a tervezési/modellezési döntések indoklását. A dokumentáció kért beadási formátuma az Adobe PDF formátum. 
• Az UPPAAL modell forrás- és követelmény- (query) fájljai.  
  Ezeket kérjük egy ZIP állományba tömöríteni.

A házi feladatok beadása:

• A házi feladat megoldását (a PDF dokumentációt és a ZIP állományba tömörített modell és követelmény leírást) kérjük emailben elküldeni Majzik István részére a majzik@mit.bme.hu címre!
• Határidő: A 4. konzultáció előtt egy héttel.

A házi feladat bemutatása

A házi feladat beadását követően kerül sor a kidolgozott feladatok bemutatására. Ennek során megbeszéljük a feladat megoldását és a beadott dokumentációt. A házi feladat értékelése a bemutatás folyamán válik véglegessé.

A házi feladat pótbeadása

A beadási határidő lezárultával feladatbeadást már csak pótbeadásként fogadunk el. A pótbeadás egy jegy levonásával jár. Aki nem ad be feladatot pótbeadással sem, az nem szerezhet félévközi jegyet.
A pótbeadási lehetőség a határidőre már beadott házi feladat módosítására nem használható fel, csak a be nem adott házi feladat pótlására vesszük azt figyelembe.

A beadandó anyagok köre megegyezik a félévközi beadáskor elvárt anyagokkal (dokumentáció, modellek, eredmények). A bemutatás része a feladat pótbedásának, ezt egyénileg egyeztetjük.

A pótbeadás ugyanolyan módon történik, mint az eredeti beadás.