Neraiškių valdymo sistemų modeliavimas ir verifikavimas atkarpomis tiesiniu agregatiniu formalizavimo metodu (Informatika 09 P)
Anotacija
Darbe pristatomas neraiškių valdymo sistemų modeliavimas ir verifikavimas atkarpomis tiesiniu agregatiniu formalizavimo metodu. Ši metodika leidžia pagal vieną formalaus modelio aprašą kurti realiojo laiko neraiškių valdymo sistemų modelius, skirtus sistemos funkcionavimo ir elgsenos analizei. Sistemų modeliavimui buvo sukurti agregatai, kurie realizuoja neraiškios sprendimo priėmimo sistemos pagrindinius komponentus. Pagal analizuojamos neraiškios valdymo sistemos struktūrą sujungus šiuos agregatus, gaunamas neraiškios sprendimo priėmimo sistemos agregatinis modelis, kuris gali būti taikomas sistemos funkcionavimo ir elgsenos analizei. Darbe taip pat pristatoma sukurta realiojo laiko agregatinių modelių verifikavimo metodika, kurią sudaro agregatinio modelio transformavimas į laiko automatus, verifikuojamų savybių užrašymas laiko logikoje bei modelių tikrinimo įrankio UPPAAL panaudojimas sistemos savybėms patikrinti.
Sukurta neraiškių valdymo sistemų modeliavimo ir verifikavimo metodika agregatiniam formalizavimo metodui buvo pritaikyta transporto srautų valdymo ir vaistų leidimo pompų sistemų analizei. Panaudojant sukurtus transporto srautų valdymo ir vaistų leidimo pompų agregatinius modelius, buvo sudaryti imitaciniai modeliai, kurie leido įvertinti modelių funkcionavimo charakteristikas ir juos tarpusavyje palyginti. Realiojo laiko agregatinių sistemų verifikavimo metodika panaudota tikrinant analizuojamų sistemų gyvybingumo, saugumo ir pasiekiamumo savybes.