Formális módszerek - Tudnivalók (2017 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.025 terem

Előadók:

Házi feladat konzulensek:

  • Vörös András: vori [at] mit.bme.hu
  • Tóth Tamás: totht [at] mit.bme.hu
  • Balogh László: laszlobalogh94 [at] gmail.com
  • Élő Dániel: contact.elodani [at] gmail.com
  • Marussy Kristóf: kris7topher [at] gmail.com
  • Soltész Adrián solteszad [at] gmail.com

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ésis 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): 7. hét
    • Első zárthelyi pótlása (PZH1): 9. hét
    • Második zárthelyi (ZH2): 13. 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. Forráskód és monitorkód generálás.
6 (Nemzeti ünnep)
7 Modellezési mintapélda. Ekvivalencia ellenőrzés.
8 Petri-hálók alapfogalmai.
9 Petri-hálók dinamikus tulajdonságai.
10 Petri-hálók strukturális tulajdonságai.
11 Adatfüggő viselkedés modlelezése: Színezett Petri-hálók.
12 Szoftver forráskód verifikációja.
13 Teljesítmény és megbízhatóság modellezése: Sztochasztikus Petri-hálók.
14 Szoftver verifikáció: Absztrakció, forráskód ellenőrzés.