Formális módszerek - Tudnivalók (2018 tavasz)

Elérhetőségek

A tárgy web lapjai:

Ajánlott jegyzet:

Előadások:

  • Minden oktatási héten szerdán 14:15-17:00, I.B.026 terem

Előadók:

Házi feladat konzulensek:

  • Graics Bence
  • Horti Norbert
  • Marussy Kristóf
  • Mezei Adrián
  • Vörös András

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

  • A félévközi jegy megszerzésének követelménye a két zárthelyi és a 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 szorgalmi feladat érdemjegye  20% súllyal pluszként számít be a félévközi jegybe (kivéve az elégtelen érdemjegyet).
    • Akinek korábbi, ötéves képzésbeli Formális módszerek félévről érvényes aláírása van, annak - amennyiben ezt kéri - nem kell házi feladatot készítenie (azt jeles osztályzattal számítjuk be a félévközi jegybe).
  • Mindkét zárthelyi pótolható, a tanulmányi teljesítményértékelés központi ütemezése szerint.
    • 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 (tehát rontani is lehet).
  • A házi feladat elkészítése kötelező. A házi feladat témája modellezés és modell alapú verifikáció.
    • A házi feladat a pótlási időszakban pótolható, a pótbeadás 20% (egy jegy) levonással jár.
    • Korábbi félévben beadott sikeres házi feladat kérésre beszámítható, ez esetben nem szükséges beadni az új feladatot (de lehetséges, ekkor az újonnan beadott feladat eredménye felülírja a régit).
    • A házi feladat beadásához bemutatás (védés) is tartozik, enélkül a beadott házifeladat nem értékelhető! A védésen röviden be kell mutatni a feladat megoldását, és 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 félév során lehetőség van egy szorgalmi feladat megoldására. Ez nem kötelező, tehát enélkül is megszerezhető a jeles félévközi jegy (ld. a fenti szabályokat). A szorgalmi feladat jegye 20% súllyal pluszként számít be a félévközi jegybe (kivéve az elégtelen érdemjegyet). A szorgalmi feladatok a Petri-hálók témaköréből kerülnek ki.
    • A szorgalmi feladat esetén nincs pótbeadási lehetőség.

A félév időbeosztása

  • Feladatok időzítése (oktatási hetek):
    • Házi feladat kiadás: 4. hét
    • Házi feladat beadás: 11. hét
    • A házi feladat védése: A 14. héten és a pótlási héten
    • Szorgalmi feladat: 14. hét
  • Zárthelyik időzítése (oktatási hetek):
    • Első zárthelyi (ZH1): 6. hét
    • Első zárthelyi pótlása (PZH1): 8. hét
    • Második zárthelyi (ZH2): 14. hét
    • Második zárthelyi pótlása (PZH2): Pótlási hét

Az előadások tervezett ütemezése

Hét Az előadás témája
1 Bevezető. Alapszintű modellezési formalizmusok.
2 Követelmény formalizálás: Temporális logikák.
3 Verifikáció: Modellellenőrzés.
4 Verifikáció: Állapottér kezelése, korlátos modellellenőrzés.
5 Mérnöki modellezés: Állapottérképek.
6 Szoftver forráskód bverifikációja absztrakcióval.
7 Petri-hálók alapfogalmai.
8 Petri-hálók dinamikus tulajdonságai.
9 Petri-hálók strukturális tulajdonságai.
10 (Oktatási szünet)
11 Adatfüggő viselkedés modlelezése: Színezett Petri-hálók.
12 Teljesítmény és megbízhatóság modellezése: Sztochasztikus Petri-hálók.
13 Petri háló modellezési példák.
14 Szorgalmi feladatok megoldása.