Communication Protocol Specification and Verification - 9781461375371

Sideprotokollid on reeglid, mille kohaselt saab sisulist suhtlust vahetada erinevate suhtlevate üksuste vahel. Üldiselt on need keerulised ning neid on keeruline kavandada ja rakendada. Loomulikus keeles (nt inglise keeles) kirjutatud suhtlusprotokollide spetsifikatsioonid võivad olla ebaselged või mitmetähenduslikud ning neid võib tõlgendada erinevalt. Selle tulemusena võivad sama protokolli sõltumatud rakendused olla ühildumatud. Lisaks muudab protokollide keerukus nende mitteametliku analüüsimise väga keeruliseks. Seetõttu on vaja täpseid ja ühemõttelisi täpsustusi, kasutades mõningaid formaalseid keeli. Paljud valdkonnas kasutatavad protokollirakendused on peaaegu kannatanud tõrgete, näiteks ummikseisu tõttu. Kui protokollide korrektse toimimise tingimusi on muudetud, pole olnud üldist meetodit nende toimimise määramiseks uutes tingimustes. Protokolli kujundajatel peavad olema tehnikad ja tööriistad vigade tuvastamiseks projekteerimise varases faasis, sest mida hiljem rike avastatakse, seda suurem on selle kõrvaldamise kulud. Protokolli kontrollimine on protsess, mille käigus kontrollitakse, kas protokolliüksuste interaktsioonid vastavalt protokolli spetsifikatsioonile tõepoolest vastavad teatud omadustele või tingimustele, mis võivad olla üldised (nt ummikseisu puudumine) või konkreetse protokollisüsteemi spetsiifilised, mis on otseselt tuletatud protokollist. spetsifikatsioon. 80ndatel alustas ISO (Rahvusvahelise Standardiorganisatsiooni) töörühm tööprogrammi, et töötada välja ametlikud keeled, mis sobivad avatud süsteemide vastastikuse sidumise (OSI) jaoks. See rühm nimetas selliseid keeli formaalseteks kirjeldusmeetoditeks (FDT). Mõned ISO eesmärgid FDT-de väljatöötamisel olid järgmised: OSI protokollistandardite ühemõtteliste, selgete ja täpsete kirjelduste kirjutamise võimaldamine ning selliste spetsifikatsioonide õigsuse kontrollimine. ISO standarditud FDT-d on kaks: LOTOS ja Estelle. Sideprotokolli spetsifikatsioon ja kontrollimine on kirjutatud kahe eespool käsitletud probleemi lahendamiseks: vajadus määrata protokoll FDT abil ja kontrollida selle õigsust, et avastada spetsifikatsioonivead protokolli arendusprotsessi varases staadiumis. Lugejaskond koosneb peamiselt edasijõudnutest bakalaureuseõppe üliõpilastest, magistriõppe üliõpilastest, kommunikatsioonitarkvara arendajatest, telekommunikatsiooniinseneridest, EDP-juhtidest, teadlastest ja tarkvarainseneridest. See on mõeldud edasijõudnute bakalaureuse- või magistriõppe õpikuks ja viitena suhtlusprotokolli spetsialistidele.