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

Elérhetőségek

A tárgy web lapjai:

Ajánlott jegyzet:

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

  • BME I. épület I.E.225. terem, a következő időpontokban: február 16., március 9., április 13. és május 4., 8:30-11:00

Anyagok a felkészüléshez:

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

Előadók:


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 (tervezet)

  • Előadások (konzultációk)
    • Február 16.: A formális módszerek szerepe. Formális modellezés. Segédanyag: T01-T02. 
    • Március 9.: Követelmények formalizálása. A modellellenőrzés. Állapottérképek. Segédanyag: T03-T06.
    • Április 13.: Petri hálók és tulajdonságaik. Segédanyag: T07-T08.
    • Május 4.: Modellezés Petri-hálókkal. Zárthelyi megírása. Házi feladat bemutatása. Segédanyag: T09-T11.
  • Zárthelyik:
    • Zárthelyi:  Május 4., az előadás időpontjában
    • Pótzárthelyi: A pótlási héten, egyénileg egyeztetett időpontban
  • Házi feladat:
    • Házi feladat kiadása: A 4. oktatási héten.
    • Házi feladat beadása: Április 28. szombat éjfélig.
    • A feladatok bemutatása: Május 4.
    • Házi feladat pótbeadása (egy jegy levonással jár): Május 23. szerda éjfélig
    • A pótbeadás bemutatása: Egyénileg egyeztetett időpontban május 25-ig.

Segédanyagok

  Téma Típus
T01 A formális módszerek szerepe Előadásfólia (PDF)
T02 Alapszintű formalizmusok Előadásfólia (PDF)
T03 Lineáris temporális logikák Előadásfólia (PDF)
T04 Elágazó idejű temporális logikák Előadásfólia (PDF)
T05 Modellellenőrzés Előadásfólia (PDF)
T06 Állapottérképek Előadásfólia (PDF)
HF Házi feladat kiírás
Házi feladathoz hasonló mintapéldák
Házi feladathoz hasonló mintapéldák modelljei
Feladatkiírás (PDF)
Mintapéldák (PDF)
Mintapéldák (ZIP)
T07 Petri hálók: alapelemek, kiterjesztések
Petri háló modellező eszköz (PetriDotNet)
Petri háló modellező eszköz dokumentáció
Példamodellek
Előadásfólia (PDF)
Eszköz (ZIP)
Dokumentáció (PDF)
Modellek (ZIP)
T08 Petri hálók tulajdonságai Előadásfólia (PDF)
T09 Petri háló alapú modellek készítése Előadásfólia (PDF)
T10 Színezett Petri hálók (kiegészítés) Előadásfólia (PDF)
T11 Modellezés színezett Petri hálókkal (példa) Előadásfólia (PDF)
ZH Ellenőrző kérdések
Gyakorló feladatok
Gyakorló feladatok megoldással
Segédanyag (PDF)
Segédanyag (PDF)
Segédanyag (PDF)

A zárthelyik

A zárthelyi:

  • Időpont: 2018. május 4. az előadás időpontjában
  • 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 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ó 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:

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.

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

  • Személyes adatok (név, Neptun kód),
  • A feladat specifikációja.

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!

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.