Opis aktivnosti

Laboratorij za mikroračunalniške sisteme

Na področju zagotavljanja pravilnosti sistemov imajo tako pristopi na podlagi akcij kot pristopi na podlagi stanj svoje dobre in slabe lastnosti. Stanjski pristop k specifikaciji in sklepanju o reverzibilnih sistemih pomeni alternativo do sedaj prevladujočim pristopom na podlagi akcij. Za sodobne omrežne tehnologije, kot so programsko določena omrežja in Internet stvari je zelo pomembno pravilno in zanesljivo delovanje. Ker sta ti tehnologiji razmeroma novi, formalne metode in orodja zanje še niso dobro razvita. Eno izmed koristnih orodij je integrirano razvojno okolje SpinRCP, ki je prosto dostopno vsem uporabnikom verifikacijskega orodja Spin. Z uvajanjem novih funkcionalnosti v SpinRCP laboratorij prispeva k razvoju znanosti in večji uporabi formalnih metod pri snovanju sodobnih omrežij in protokolov.