Communication Protocol Specification and Verification - 9781461375371

Protokoły komunikacyjne to reguły, dzięki którym możliwa jest wymiana znaczącej komunikacji pomiędzy różnymi komunikującymi się jednostkami. Ogólnie rzecz biorąc, są one złożone i trudne do zaprojektowania i wdrożenia. Specyfikacje protokołów komunikacyjnych napisane w języku naturalnym (np. angielskim) mogą być niejasne lub niejednoznaczne i mogą podlegać różnym interpretacjom. W rezultacie niezależne implementacje tego samego protokołu mogą być niekompatybilne. Ponadto złożoność protokołów sprawia, że bardzo trudno je analizować w sposób nieformalny. Istnieje zatem potrzeba precyzyjnej i jednoznacznej specyfikacji przy użyciu niektórych języków formalnych. Wiele implementacji protokołów stosowanych w terenie prawie ucierpiało z powodu awarii, takich jak zakleszczenia. W przypadku zmiany warunków, w których protokoły działają prawidłowo, nie ma ogólnej metody pozwalającej określić, jak będą one działać w nowych warunkach. Projektanci protokołów muszą dysponować technikami i narzędziami umożliwiającymi wykrywanie błędów we wczesnej fazie projektowania, ponieważ im później w procesie zostanie wykryta usterka, tym większy będzie koszt jej naprawienia. Weryfikacja protokołu to proces sprawdzania, czy interakcje jednostek protokołu, zgodnie ze specyfikacją protokołu, rzeczywiście spełniają pewne właściwości lub warunki, które mogą być albo ogólne (np. brak zakleszczenia), albo specyficzne dla konkretnego systemu protokołu wywodzące się bezpośrednio z specyfikacja. W latach 80. grupa robocza ISO (Międzynarodowa Organizacja Normalizacyjna) rozpoczęła program prac mający na celu opracowanie języków formalnych odpowiednich dla wzajemnych połączeń systemów otwartych (OSI). Grupa ta nazwała takie języki technikami opisu formalnego (FDT). Niektóre z celów ISO przy opracowywaniu FDT obejmowały: umożliwienie pisania jednoznacznych, jasnych i precyzyjnych opisów standardów protokołów OSI oraz umożliwienie weryfikacji poprawności takich specyfikacji. Istnieją dwa FDT standaryzowane przez ISO: LOTOS i Estelle. Specyfikacja i weryfikacja protokołu komunikacyjnego została napisana, aby zająć się dwoma kwestiami omówionymi powyżej: potrzebą określenia protokołu za pomocą FDT i sprawdzenia jego poprawności w celu wykrycia błędów specyfikacji na wczesnym etapie procesu opracowywania protokołu. Czytelnicy składają się głównie z zaawansowanych studentów studiów licencjackich, studentów studiów podyplomowych, twórców oprogramowania komunikacyjnego, inżynierów telekomunikacji, menedżerów EDP, badaczy i inżynierów oprogramowania. Jest pomyślany jako zaawansowany podręcznik dla studentów studiów licencjackich i podyplomowych oraz źródło informacji dla specjalistów zajmujących się protokołami komunikacyjnymi.