English
Magyar
HF4. Együttműködés ellenőrzése
Beküldési határidő: 2019. május. 29. 23:59 (érdemes előbb, hogy küldhessünk visszajelzést)
Személyes bemutatás: 2019. május 30-ig (Vörös Andrással emailben egyeztetett időpontban)
Becsült idő: 4-5 óra
Formális módszerek alkalmazása együttműködő folyamatok ellenőrzésére
Napjaink komplex rendszerei komoly tervezést igényelnek. Azonban nem elég megtervezni egy rendszert, a rendszertervek ellenőrzése is szükséges, hogy megbizonyosodhassunk a helyes működésről. Különösen fontos ez az olyan kritikus rendszerek esetén, mint az elosztott felhő alapú szolgáltatások vagy a biztonságkritikus beágyazott rendszerek. Ebben segítenek nekünk a formális módszerek, amelyek a matematika eszköztárát használják fel a tervek helyességének precíz vizsgálata során.
Különösen nehéz feladat elosztott, párhuzamos és együttműködő folyamatok/rendszerek tervezése: egyre több cég vet be formális módszereket a fejlesztési folyamatban (lásd például: http://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf).
A fakultatív feladat során a hallgató feladata a kiadott kölcsönös kizárást megvalósító pszeudo kódok ellenőrzése holtpontmentesség és a kölcsönös kizárás biztosítás szempontjából.
A modellezés megkönnyítése érdekében rendelkezésre áll egy saját tutorial (de persze érdemes használni az UPPAAL oldalán elérhető hivatalos tutorialokat is): https://www.mit.bme.hu/system/files/oktatas/targyak/10746/opre_imsc_labor_uppaal_handout.pdf
A feladat: minden egyes példára modellezéssel és az UPPAAL modellellenőrző eszköz használatával megvizsgálni, hogy teljesül-e a kölcsönös kizárás, a holtpontmentesség, továbbá teljesül-e, hogy ha egy részt vevő be akar lépni a kritikus szakaszba, akkor garantáltan beléphet-e. Az első feladatok bemelegítő jellegűek és nagyon egyszerűek, a feladatsor vége bonyolultabb feladatokat tartalmaz.
Bármilyen kérdés esetén Vörös Andrást keressétek, továbbá a feladatok bemutatása is nála lehetséges (személyes bemutatás).
A fakultatív feladat elvégzésében segíthet a "Formális módszerek alkalmazása együttműködő folyamatok ellenőrzésére" laboron való részvétel, ahol feladatmegoldás során lehet gyakorolni (és iMSc pontokat szerezni)
A a fakultatív feladat elkészítését az UPPAAL eszközben javasoljuk, azonban más modellellenőrző eszköz is használható, azonban konzultációs segítséget UPPAAL és PetriDotNet használata esetén tudunk csak biztosítani.
Érdeklődők számára lehetőség van kipróbálni az elmúlt években az egyetemen fejlesztett PetriDotNet modellező és analízis keretrendszert is: https://inf.mit.bme.hu/research/tools/petridotnet
Beadás: e-mailben elküldve Vörös András részére a határidő napján éjfélig. Minden elküldött házit személyesen is be kell mutatni, meg kell védeni, erről e-mailben tájékoztatást küldök, hogy pontosan mikor és hol (kb 10--15 percben mindenkit kérek, hogy magyarázza el, hogy miért úgy modelllezett, és az ellenőrzés eredményeit is megtekintjük, ez alapján válik véglegessé a házi feladat pontszám)
