I protocolli di comunicazione sono regole in base alle quali è possibile scambiare comunicazioni significative tra diverse entità comunicanti. In generale, sono complessi e difficili da progettare e implementare. Le specifiche dei protocolli di comunicazione scritti in una lingua naturale (ad esempio l'inglese) possono essere poco chiare o ambigue e possono essere soggette a diverse interpretazioni. Di conseguenza, implementazioni indipendenti dello stesso protocollo potrebbero essere incompatibili. Inoltre, la complessità dei protocolli li rende molto difficili da analizzare in modo informale. Esiste quindi la necessità di specificazioni precise e inequivocabili utilizzando alcuni linguaggi formali. Molte implementazioni di protocolli utilizzate sul campo hanno quasi subito fallimenti, come ad esempio situazioni di stallo. Quando le condizioni in cui i protocolli funzionano correttamente sono state modificate, non è stato disponibile alcun metodo generale per determinare come funzioneranno nelle nuove condizioni. È necessario che i progettisti del protocollo dispongano di tecniche e strumenti per rilevare gli errori nella fase iniziale della progettazione, perché più tardi nel processo viene scoperto un errore, maggiore è il costo per correggerlo. La verifica del protocollo è un processo di verifica se le interazioni delle entità del protocollo, secondo la specifica del protocollo, soddisfano effettivamente determinate proprietà o condizioni che possono essere generali (ad esempio, assenza di deadlock) o specifiche per il particolare sistema di protocollo direttamente derivato dalla specifica. Negli anni '80 un gruppo di lavoro dell'ISO (Organizzazione Internazionale per la Standardizzazione) iniziò un programma di lavoro per sviluppare linguaggi formali adatti all'Interconnessione di Sistemi Aperti (OSI). Questo gruppo ha chiamato tali linguaggi tecniche di descrizione formale (FDT). Alcuni degli obiettivi dell'ISO nello sviluppo delle FDT erano: consentire la scrittura di descrizioni inequivocabili, chiare e precise degli standard del protocollo OSI e consentire la verifica della correttezza di tali specifiche. Esistono due FDT standardizzati dall'ISO: LOTOS ed Estelle. Specifica e verifica del protocollo di comunicazione è scritto per affrontare le due questioni discusse sopra: la necessità di specificare un protocollo utilizzando un FDT e di verificarne la correttezza per scoprire errori di specifica nella fase iniziale del processo di sviluppo di un protocollo. Il pubblico dei lettori è costituito principalmente da studenti universitari di livello avanzato, studenti post-laurea, sviluppatori di software di comunicazione, ingegneri delle telecomunicazioni, manager EDP, ricercatori e ingegneri del software. È inteso come un libro di testo universitario o post-laurea avanzato e un riferimento per i professionisti del protocollo di comunicazione.
caricamento...
