Formális módszerek - GTK levelező képzés (2017 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.412. terem, a következő időpontokban: febr. 24., márc. 24., ápr. 21. és máj. 12., 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 két zárthelyi és egy házi feladat legalább elégséges szintű teljesítése.
  • A félévközi jegyet 35-35%-os súllyal a két zárthelyi osztályzata, 30%-os súllyal pedig a házi feladat osztályzata határozzák meg.
    • Mindkét zárthelyire és a házi feladatra is jegyet kap minden hallgató.
    • Mindhárom jegyre érvényes, hogy az elégséges szintet el kell érnie.
    • A kapott jegyekből a fenti 35-35-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 24.: A formális módszerek szerepe. Formális modellezés. Segédanyag: T01-T02. 
    • Március 24.: Követelmények formalizálása. A modellellenőrzés. Állapottérképek. Segédanyag: T03-T06.
    • Április 21.: ZH1. Petri hálók és tulajdonságaik. Segédanyag: T07-T08.
    • Május 12.: Modellezés Petri-hálókkal. ZH2. Házi feladat bemutatása. PótZH1. Segédanyag: T09-T11.
  • Zárthelyik:
    • Zárthelyi (első):  Április 21. az előadás időpontjában
    • Zárthelyi (második): Május 12. az előadás időpontjában
    • Pótzárthelyi (első): Május 12. az előadás időpontjában
    • Pótzárthelyi (második): Egyénileg egyeztetett időpontban.
  • Házi feladat:
    • Házi feladat kiadása: A 4. oktatási héten (február 27-től).
    • Házi feladat beadása: Május 6. szombat éjfélig.
    • A feladatok bemutatása: Május 12.
    • Házi feladat pótbeadása (egy jegy levonással jár): Május 17. szerda éjfélig
    • A pótbeadás bemutatása: Egyénileg egyeztetett időpontban május 19-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)
ZH1 ZH1 ellenőrző kérdések
ZH1 gyakorló feladatok
ZH1 gyakorló feladatok megoldással
ZH1 kiegészítő háttéranyag: Temporális logikák
ZH1 kiegészítő háttéranyag: Állapottérképek
Segédanyag (PDF)
HF1 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)
ZH2 ZH2 ellenőrző kérdések
ZH2 gyakorló feladatok
ZH2 gyakorló feladatok megoldással
Segédanyag (PDF)

A zárthelyik

Az első zárthelyi:

  • Időpont: 2017. április 21. az előadás időpontjában
  • Témája: A fenti segédanyagok között megtalálható T01 - T06 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 ZH1 anyagai 
  • A felkészüléshez használható mintapéldák: A fenti segédanyagok között a ZH1 anyagai

A második zárthelyi

  • Időpont: 2017. május 12. az előadás időpontjában
  • Témája: A fenti segédanyagok között megtalálható T07 - T09 témák
  • A felkészüléshez használható mintapéldák: A fenti segédanyagok között a ZH2 anyagai

Az első pótzárthelyi:

  • Időpont: 2017. május 12. az előadás időpontjában
  • Témája: Az első zárthelyi pótolható.

A második pótzárthelyi:

  • A második pótzárthelyi időpontját és helyszínét egyénileg egyeztetjük.
  • Témája: Bármelyik sikertelen zárthelyi akár ismételten is pótolható, vagy sikeres zárthelyi javítható.

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 HF1 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.