Formális módszerek - Házi feladat (2020 tavasz)

Tartalom:

• Eszközök
• Feladatkiírások
• Konzultáció
• Beadás
• Bemutatás
• Pótbeadás
• Eredmények

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.

A házi feladat megoldása során egy szöveges leírással megadott rendszerhez kell formális modellt készíteni, majd a modellen adott követelmények teljesülését kell modellellenőrzéssel igazolni.

• A feladatban megadott rendszert (időzített) automatákkal kell modellezni az UPPAAL eszköz segítségével.
• A megadott követelményeket temporális logikai kifejezésekkel kell formalizálni és az UPPAAL verifikációs moduljának segítségével kell ellenőrizni.

Célunk, hogy mindenki gyakorlatot szerezzen a formális modellezésben és verifikációban. A formális modell elkészítése többféle módon is helyes lehet; a feladatok értelmezésekor elvárjuk, hogy az informális leírásban foglaltaknak feleljen meg a kidolgozott formális modell.

A házi feladat teljesítésének lépései tipikusan a következők:

1. A szövegesen megadott rendszernek készítse el a formális modelljét az UPPAAL rendszerben.
   • 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 (ha valami nem egyértelmű) 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.
   • Dokumentálja a verifikáció eredményé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. Mivel korlátozott számú feladattípus kerül kiadásra, így egy-egy feladatot több hallgató is megkap. 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 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 Információs Technológia Tanszéke és a dániai Aalborg Egyetem Számítástudományi Tanszéke 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 elosztott rendszerek modellezésére együttműködő időzített automaták hálózata 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 (határolt egészek, tömbök, stb.) és egyszerű függvények 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) is 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. 

• Internet Explorer 9 esetén problémákat jeleztek a regisztráció és letöltés során, ez esetben másik böngészővel is érdemes próbálkozni.
• Ha a telepített stabil verzió licensz problémákat jelez, akkor érdemes a fejlesztői verziót használni, vagy időnként a BME IP címtartományában futtatni (a licensz fájl frissítéséhez).

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, ezeket ajánlott tanulmányozni:

• 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 átnézése, kipróbálása, valamint az eszköz Help menüjéből elérhető leírás átolvasása.

A házi feladatok hallgatókhoz rendelése és a feladatkiírások

Minden hallgató egyénileg kap feladatot.

• A házi feladat kódja a hf.mit.bme.hu portálra belépve található meg.
  Ugyanezt a portált kell használni az elkészült megoldás beadására is.
• Aki kéri, hogy korábbi félévben sikeresen beadott házi feladatát fogadjuk el, annak nem kell az új feladatot beadnia.

Az egyes feladatkiírások és a feladatok konzulensei a következő táblázatban találhatók.

Konzultációs lehetőség

A 10. és 11. oktatási héten (a feladat beadási határidejét megelőzően) konzultációs lehetőséget ajánlunk fel, ekkor tehetik fel a feladattal kapcsolatos kérdéseiket az adott feladat konzulensének az érdeklődő hallgatók.

A konzultáció nem kötelező, viszont kérjük, akinek kérdése van, lehetőleg a felajánlott módokon és időpontokban keresse a konzulensét.

A konzultációs időpontok az alábbi táblázatban lesznek találhatók. A további részletekről Neptun üzenetet küldünk.

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 részletes dokumentációja (ábrákkal ellátott szöveges leírás) a fenti megoldási lépések szerint. A dokumentáció tartalmazza a modell felépítésének ismertetését, a formalizált követelményeket, valamint azok ellenőrzésének eredményét, valamint a 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.  

Mindezeket kérjük egy ZIP állományba tömöríteni.

Kérjük, hogy a dokumentációban mindenképpen szerepeljenek a következők:

• A személyes adatok (név, Neptun kód),
• Egy nyilatkozat arról, hogy a feladat megoldása önállóan, meg nem engedett segédeszközök nélkül történt.

A házi feladatok beadása elektronikus úton történik a hf.mit.bme.hu portálon.

Beadási határidő:  2020. május 9. szombat, 23:59:00 (a portál rögzíti a beadás időpontját). 

A beadási határidő lezárultával feladatbeadást már csak pótbeadásként fogadunk el.

A házi feladat bemutatása

A házi feladat beadását követően a konzulens kérheti a feladat megoldásának személyes (online) bemutatását. Ennek során válaszolni kell a konzulens által 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, és próbálják az önálló munkát ellenőrizni.

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 20% (egy jegy) levonással jár. Aki nem ad be feladatot pótbeadással sem, az nem szerezhet félévközi jegyet!

A pótbeadás elektronikus úton történik a hf.mit.bme.hu portálon.

Pótbeadási határidő: 2020. május 27. szerda, 23:59:00  A vizsgaidőszak 10. napja.

A beadandó anyagok köre megegyezik a félévközi beadáskor elvárt anyagokkal (dokumentáció, modellek, eredmények). A pótbeadás során beadott házi feladat esetén is kérhetünk személyes bemutatást.

Már beadott, értékelt és elfogadott házi feladat javító célzattal történő ismételt beadását nem fogadjuk el. Aki javítani szeretne a házi feladat jegyén, jelezze a tárgyfelelősnek emailben, és számára új feladatot adunk ki. Ennek beadási határideje is a fenti pótbeadási határidő. 

A házi feladatok eredményei

A házi feladatok értékelései és jegyei elektronikus úton hozzáférhetők a hf.mit.bme.hu portálon.