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

Tartalom:

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 rendszert kell formális modellel leírni, 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 forgatókönyve az alábbi.

  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 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ó 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 tervezés során a modell kidolgozása lépésenkénti finomítással célszerű, dokumentálva az egyes lépéseket.

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 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 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 hivatalos 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:

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ó a Neptun kódja alapján keresheti meg a kidolgozandó házi feladatát:

  • Házi feladatok hallgatókhoz rendelése: Neptun kódok és házi feladat sorszámok itt voltak találhatók.
  • Aki kérte, és elfogadtuk a korábbi félévben sikeresen megvédett házi feladatát, annak nem kell az új feladatot beadnia.

Az egyes házi feladatok konkrét megfogalmazása (azaz a modellezendő rendszer és a hozzá kapcsolódó ellenőrizendő követelmények leírása), valamint a feladat kidolgozását segítő konzulens neve itt olvasható:

Sorszám A feladat címe A feladat konzulense
HF01 Kávéautomata Graics Bence
HF02 Közlekedési lámpák vezérlése Graics Bence
HF03 Cipőgyár Horti Norbert
HF04 TicTacToe Horti Norbert
HF05 Sudoku Mezei Adrián
HF06 Webshop Mezei Adrián
HF07 Flexibilis gyártócella Marussy Kristóf
HF08 Romulán béketárgyalások Marussy Kristóf
HF09 Elosztott fürtrendszer Vörös András
HF10 Időzített mutex (javított) Vörös András

 

 

Konzultációs lehetőség

A 9. vagy 10. oktatási héten (a feladat beadási határidejét megelőzően) konzultációs időpontokat 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ókon való megjelenés nem kötelező, viszont kérjük, akinek kérdése van, lehetőleg ezekben az időpontokban keresse a konzulensét. Akinek órarendi ütközés miatt nem lenne alkalmas a megadott konzultációs időpont, kérjük, hogy e-mailben keresse meg a tárgyfelelőst.

A konzultációs időpontok és helyszínek az alábbi táblázatban találhatók.

Sorszám A feladat konzulense Konzultáció
HF01 Graics Bence I.L.405 terem, 2018. ápr. 11. szerda, 13-14
HF02 Graics Bence I.L.405 terem, 2018. ápr. 11. szerda, 13-14
HF03 Horti Norbert I.L.405 terem, 2018. ápr. 11. szerda, 17-18
HF04 Horti Norbert I.L.405 terem, 2018. ápr. 11. szerda, 17-18
HF05 Mezei Adrián I.L.405 terem, 2018. ápr. 13. péntek, 12-13
HF06 Mezei Adrián I.L.405 terem, 2018. ápr. 13. péntek, 12-13
HF07 Marussy Kristóf I.L.405 terem, 2018. ápr. 11. szerda, 17-18
HF08 Marussy Kristóf I.L.405 terem, 2018. ápr. 11. szerda, 17-18
HF09 Vörös András I.L.405 terem, 2018. ápr. 13. péntek, 12-13
HF10 Vörös András I.L.405 terem, 2018. ápr. 13. péntek, 12-13

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 forgatókönyv szerint.
    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 és 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 lekérdezési (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),
  • A feladat címe (nemcsak a sorszáma!).

A házi feladatok beadása elektronikus űrlap segítségével történik, a Házi feladatok és jegyzőkönyvek leadása (útmutató) oldalon leírtak szerint.

Beadási határidő:  2018. április 28. szombat, 23:59:00 (a beadó űrlap 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 pótbeadáshoz a beadó űrlapot újra megnyitjuk, a részleteket ld. lejjebb!

A házi feladat bemutatása

A házi feladat beadását követően kerül sor a kidolgozott feladatok személyes bemutatására (védésére). Ennek célja annak megállapítása, hogy a hallgató önállóan, saját munkával és a megengedett eszközöket felhasználva készítette el a feladatát. A védés során néhány percben rövid kérdéseket teszünk fel a modellezési feladattal és a beadott dokumentációval kapcsolatban. A házi feladat értékelése a védés folyamán válik véglegessé.

A feladatok védése az egy konzulensre eső hallgatók magas száma miatt több órás program, amelynek időbeosztására, azaz az adott hallgató védésének konkrét időpontjára előzetesen jelentkezni kell.

A házi feladatok védéseinek ütemezése és a jelentkezések az alábbi táblázatban találhatók.

  • Kérünk mindenkit, hogy a jelentkezési űrlapon a házi feladatához EGY blokkot foglaljon le.
  • Akik pótbeadásként adják be a házi feladatukat, azok a pótlási időszakban megadott pótvédésre jelentkezzenek (egyes feladatok esetén ezek időpontjai később kerülnek ki). Szintén a pótvédésre jelentkezzenek, akik órarendi okok vagy helyhiány miatt nem tudnak jelentkezni a szorgalmi időszakban szervezett védésre.
  • A védésen kötelező személyesen megjelenni. Aki a védésen nem jelenik meg, annak a házi feladatát nem fogadjuk el. Ha a jelentkezéssel kiválasztott időpontban a megjelenésnek komoly akadálya merül fel, keressék meg a tárgyfelelőst új időpont egyeztetése céljából.
  • A KT jelölés az IB420 szoba előtti körtárgyalót jelenti, a másik lehetséges helyszín az IL405 labor (lásd az egyes időpontoknál). 
Sorszám A feladat konzulense Jelentkezés védési időpontra Jelentkezés pótvédésre
HF01 Graics Bence 2018. május 16, 17:00-19:30, IL405
https://doodle.com/poll/yucfntnwxztervdh
2018. május 24, 16:00-18:00, IL405
https://doodle.com/poll/yucfntnwxztervdh
HF02 Graics Bence 2018. május 16, 17:00-19:30, IL405
https://doodle.com/poll/yucfntnwxztervdh
2018. május 24, 16:00-18:00, IL405
https://doodle.com/poll/yucfntnwxztervdh
HF03 Horti Norbert 2018. május 16, 12:00-13:30, IL405
2018. május 17, 12:30-14:00, KT
2018. május 18, 12:00-13:00, KT
2018. május 22, 12:00-14:00, IL405
https://doodle.com/poll/tgagsd3mz94ywncb
2018. május 24, 16:00-18:00, IL405
https://doodle.com/poll/pkb2t7sp2v7bed32
HF04 Horti Norbert 2018. május 16, 12:00-13:30, IL405
2018. május 17, 12:30-14:00, KT
2018. május 18, 12:00-13:00, KT
2018. május 22, 12:00-14:00, IL405
https://doodle.com/poll/tgagsd3mz94ywncb
2018. május 24, 16:00-18:00, IL405
https://doodle.com/poll/pkb2t7sp2v7bed32
HF05 Mezei Adrián 2018. május 24, 13:20-17:10, IL405
https://doodle.com/poll/g44amq49y49qqk9w
2018. május 24, 13:20-17:10, IL405
https://doodle.com/poll/g44amq49y49qqk9w
HF06 Mezei Adrián 2018. május 24, 13:20-17:10, IL405
https://doodle.com/poll/g44amq49y49qqk9w
2018. május 24, 13:20-17:10, IL405
https://doodle.com/poll/g44amq49y49qqk9w
HF07 Marussy Kristóf 2018. május 16, 14:00-19:00, IL405
https://doodle.com/poll/hnzze3p3xxs9g37s
2018. május 24, 14:00-19:00, IL405
https://doodle.com/poll/u8ckmhmygxmytvr2
HF08 Marussy Kristóf 2018. május 16, 14:00-19:00, IL405
https://doodle.com/poll/hnzze3p3xxs9g37s
2018. május 24, 14:00-19:00, IL405
https://doodle.com/poll/u8ckmhmygxmytvr2
HF09 Vörös András 2018. május 15, 12:00-14:30, KT
2018. május 16, 14:00-16:00, IL405
https://doodle.com/poll/e6c435kizh6c44p5
2018. május 25, 9:00-10:00, IL405
https://doodle.com/poll/2sz76gmgxwr5nhaf
HF10 Vörös András 2018. május 15, 12:00-14:30, KT
2018. május 16, 14:00-16:00, IL405
https://doodle.com/poll/e6c435kizh6c44p5
2018. május 25, 9:00-10:00, IL405
https://doodle.com/poll/2sz76gmgxwr5nhaf

 

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 űrlap segítségével történik, a Házi feladatok és jegyzőkönyvek leadása (útmutató) oldalon leírtak szerint.

Pótbeadási határidő: 2018. május 23. szerda, 23:59:00  (a beadó űrlap rögzíti a beadás időpontját).

A beadandó anyagok köre megegyezik a félévközi beadáskor elvárt anyagokkal (dokumentáció, modellek, eredmények). A védés része a feladat bedásának, erre még a pótlási időszakban sor kerül.

A pótvédések időpontja: A pótvédések időpontjai a normál védésekkel együtt vannak meghirdetve (ld. fentebb).
Ugyanekkor a korábban beadott házi feladatok esetlegesen elmaradt védései is pótolhatók.

A házi feladatok eredményei

A házi feladatok jegyei a védéseken válnak véglegessé.