Formal specification and verification of the OSI session layer using the Calculus of Communicating Systems (CCS)
Date of Award
Doctor of Philosophy (PhD)
Electrical Engineering and Computer Science
Electrical engineering, Computer science
Digital Communications and Networking
This document describes the application of formal methods to concurrent software systems, specifically communication protocols. The chosen formal method is Milner's process algebra called the Calculus of Communicating Systems (CCS). We applied CCS to the specification and verification of the Open Systems Interconnection (OSI) Session Layer (SL). We modeled the Session Layer service and Session Layer protocol in CCS, and verified it using CCS's automated model checker, the Edinburgh Concurrency Workbench (CWB). We verified that the protocol specification satisfies the service specification. We also formally embedded CCS in the first-order formal language Larch, using the automated theorem prover Penelope. We tested the embedding by specifying and verifying a simple two-slot buffer example. We compared the automated tools by specifying a portion of the Session Layer and verifying it using Penelope.
Surface provides description only. Full text is available to ProQuest subscribers. Ask your Librarian for assistance.
Barjaktarovic, Milica, "Formal specification and verification of the OSI session layer using the Calculus of Communicating Systems (CCS)" (1995). Electrical Engineering and Computer Science - Dissertations. Paper 195.