Kritikus protokollok modellezése
A feladat célja a kritikus beágyazott rendszerekben használt protokollok (pl. kapcsolatfelvétel és kapcsolatfenntartás, üzenetküldés veszteséges csatornán, konzisztens döntéshozatal) modellezésére alkalmas eszközök és modellezési nyelvek megismerése, majd ezek alkalmazása kiválasztott protokollok modell alapú ellenőrzésére. A modellezendő protokollok ipari partnerektől származó, valós megoldások.
Lényeges kihívásokat jelentenek a következők: üzenet időbélyegek és időfüggő viselkedés modellezése, üzenetvesztés modellezése, csatorna késleltetések modellezése, időszinkronizáció kezelése, bizánci jellegű (félrevezető, rosszindulatú) hibák modellezése.
A feladat megoldása során nemcsak a modellezési ynelvek és eszkjözök ismerhetők meg, hanem a valós rendszerekben alkalmazott protokollok jellegzetes megoldásai, valamint a precíz ellenőrzés technikái is (modellellenőrzés, szimuláció, szisztematikus tesztgenerálás).