Communication Protocol Specification and Verification - 9781461375371

Komunikācijas protokoli ir noteikumi, ar kuriem starp dažādām saziņas entītijām var apmainīties ar jēgpilnu saziņu. Kopumā tie ir sarežģīti un grūti projektējami un īstenojami. Dabiskā valodā (piemēram, angļu valodā) rakstīto komunikācijas protokolu specifikācijas var būt neskaidras vai neskaidras, un tās var tikt dažādi interpretētas. Rezultātā viena un tā paša protokola neatkarīgas implementācijas var būt nesaderīgas. Turklāt protokolu sarežģītības dēļ tos ir ļoti grūti analizēt neformālā veidā. Tāpēc ir nepieciešama precīza un nepārprotama specifikācija, izmantojot dažas formālas valodas. Daudzas laukā izmantotās protokolu ieviešanas ir gandrīz cietušas no kļūmēm, piemēram, strupceļiem. Kad ir mainīti apstākļi, kādos protokoli darbojas pareizi, nav pieejama vispārēja metode, kā noteikt, kā tie darbosies jaunajos apstākļos. Protokolu izstrādātājiem ir jābūt paņēmieniem un instrumentiem, lai atklātu kļūdas agrīnā projektēšanas fāzē, jo, jo vēlāk tiek atklāta kļūme, jo lielākas ir tās novēršanas izmaksas. Protokola pārbaude ir process, kurā pārbauda, vai protokola entītiju mijiedarbība saskaņā ar protokola specifikāciju patiešām atbilst noteiktām īpašībām vai nosacījumiem, kas var būt vispārīgi (piemēram, strupceļa neesamība) vai specifiski konkrētajai protokola sistēmai, kas tieši izriet no protokola specifikācija. 80. gados ISO (Starptautiskā standartizācijas organizācija) darba grupa uzsāka darba programmu, lai izstrādātu formālas valodas, kas būtu piemērotas atvērto sistēmu starpsavienojumam (OSI). Šī grupa šādas valodas sauca par formālajām apraksta metodēm (FDT). Daži no ISO mērķiem, izstrādājot FDT, bija: nodrošināt nepārprotamus, skaidrus un precīzus OSI protokolu standartu aprakstus un ļaut pārbaudīt šādu specifikāciju pareizību. Ir divi ISO standartizēti FDT: LOTOS un Estelle. Sakaru protokola specifikācija un pārbaude ir rakstīta, lai risinātu divus iepriekš apspriestos jautājumus: nepieciešamību norādīt protokolu, izmantojot FDT, un pārbaudīt tā pareizību, lai atklātu specifikācijas kļūdas protokola izstrādes procesa sākumposmā. Lasītāju loku galvenokārt veido progresīvi bakalaura studenti, pēcdiploma studenti, komunikācijas programmatūras izstrādātāji, telekomunikāciju inženieri, EDP vadītāji, pētnieki un programmatūras inženieri. Tā ir paredzēta kā uzlabota bakalaura vai pēcdiploma mācību grāmata un atsauce komunikācijas protokola profesionāļiem.