Kompiuterinių tinklų protokolų formalusis specifikavimas ir analizė: agregatinis metodas (el. knyga) (skaityta knyga) | knygos.lt

Aprašymas

Monografijoje pateikiamas paskirstytųjų sistemų formalizavimo ir analizės metodas, kurio teorinis pagrindas - atkarpomis tiesinių agregatų formalizmas. Ši matematinė schema leidžia bendrosios formaliosios specifikacijos pagrindu validuoti sudarytą specifikaciją (atlikti teisingumo analizę) bei sudaryti analizuojamos sistemos imitacinį modelį. Atkarpomis tiesiniai agregatai priklauso automatų modelių klasei. Skiriamasis šių modelių bruožas yra sistemos būsenai aprašyti naudojamos diskrečiosios ir tolydžiosios koordinatės. Atkarpomis tiesiniai agregatai aprašomi valdymo sekų metodu. Pateikiami pasiekiamų būsenų ir invariantinis agregatinių specifikacijų teisingumo tikrinimo metodai. Jie leidžia analizuoti specifikuotos sistemos saugumo ir gyvybingumo savybes. Saugumo charakteristikos rodo, kad sistemoje neįvyksta iš anksto apibrėžtų nepageidaujamų įvykių. Tokių įvykių pavyzdžiai gali būti: statinės ir dinaminės aklavietės, kintamųjų apibrėžtumas, invariantinės savybės ir pan. Gyvybingumo charakteristikos rodo, kad sistemoje įvyksta tam tikrų pageidaujamų įvykių. Pasiekiamų būsenų metodo esmę sudaro tai, kad, turint analizuojamos sistemos agregatinę specifikaciją, generuojama visų galimų sistemos būsenų trajektorijų aibė. Paskui šios trajektorijos analizuojamos sistemos tiriamų savybių atžvilgiu. Taikant invariantų metodą, reikia sudaryti sistemos invariantą ir patikrinti, ar jis yra teisingas visose galimose sistemos būsenose. Pateikiama aptarnavimo sistemų bei kompiuterių tinklų protokolų formaliojo specifikavimo, teisingumo tikrinimo ir imitacinio modeliavimo, taikant monografijoje pateiktą formalizavimo metodą, pavyzdžių. Monografija skirta Informatikos ir Telekomunikacijų ir elektronikos fakultetų magistrantams ir doktorantams, vykdantiems mokslinius tyrimus paskirstytųjų informacinių sistemų bei kompiuterių tinklų protokolų formalizavimo ir analizės mokslo kryptyje.