Az előadás bemutatja, hogy milyen módszerekkel lehet feladatok közötti kommunikációt megvalósító algoritmusokat leírni, majd azokat szimulálni és ellenőrizni. Az előadásban az UPPAAL és a PetriDotNet eszközöket fogjuk használni ilyen algoritmusok verifikálására.