Communication Protocol Specification and Verification - 9781461375371

Ryšio protokolai yra taisyklės, pagal kurias tarp skirtingų bendraujančių subjektų galima keistis reikšmingu ryšiu. Apskritai jie yra sudėtingi, juos sunku suprojektuoti ir įgyvendinti. Natūralia kalba (pvz., anglų) parašytų komunikacijos protokolų specifikacijos gali būti neaiškios arba dviprasmiškos, gali būti skirtingai interpretuojamos. Dėl to nepriklausomi to paties protokolo diegimai gali būti nesuderinami. Be to, dėl protokolų sudėtingumo juos labai sunku analizuoti neoficialiai. Todėl naudojant kai kurias formalias kalbas reikia tikslių ir nedviprasmiškų specifikacijų. Daugelis šioje srityje naudojamų protokolų diegimų beveik nukentėjo nuo gedimų, tokių kaip aklavietė. Kai buvo pakeistos sąlygos, kuriomis protokolai veikia tinkamai, nebuvo bendro metodo, kaip nustatyti, kaip jie veiks naujomis sąlygomis. Protokolų kūrėjams būtina turėti metodus ir įrankius, leidžiančius aptikti klaidas ankstyvoje projektavimo fazėje, nes kuo vėliau gedimas aptinkamas, tuo didesnės jo pašalinimo išlaidos. Protokolo tikrinimas – tai procesas, kuriuo tikrinama, ar protokolo objektų sąveika pagal protokolo specifikaciją iš tiesų atitinka tam tikras savybes arba sąlygas, kurios gali būti bendros (pvz., aklavietės nebuvimas) arba specifinės konkrečiai protokolo sistemai, tiesiogiai išvestos iš protokolo. specifikacija. Devintajame dešimtmetyje ISO (Tarptautinės standartizacijos organizacijos) darbo grupė pradėjo darbo programą, kuria siekiama sukurti oficialias kalbas, tinkamas atvirų sistemų sujungimui (OSI). Ši grupė tokias kalbas pavadino formaliojo aprašymo technikomis (FDT). Kai kurie ISO tikslai kuriant FDT buvo šie: sudaryti galimybę parašyti nedviprasmiškus, aiškius ir tikslius OSI protokolų standartų aprašymus ir leisti patikrinti tokių specifikacijų teisingumą. Yra du ISO standartizuoti FDT: LOTOS ir Estelle. Ryšio protokolo specifikacija ir tikrinimas yra parašytas siekiant išspręsti dvi aukščiau aptartas problemas: poreikį nurodyti protokolą naudojant FDT ir patikrinti jo teisingumą, kad būtų galima atskleisti specifikacijų klaidas ankstyvoje protokolo kūrimo proceso stadijoje. Skaitytojų auditoriją daugiausia sudaro pažengę bakalauro studijų studentai, magistrantūros studentai, komunikacijos programinės įrangos kūrėjai, telekomunikacijų inžinieriai, EDP vadovai, mokslininkai ir programinės įrangos inžinieriai. Jis skirtas kaip pažangus bakalauro ar antrosios pakopos studijų vadovėlis ir nuoroda komunikacijos protokolo specialistams.