Title

Formal specification and verification of the OSI session layer using the Calculus of Communicating Systems (CCS)

Date of Award

1995

Degree Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

Department

Electrical Engineering and Computer Science

Advisor(s)

Shiu-Kai Chin

Keywords

Electrical engineering, Computer science

Subject Categories

Digital Communications and Networking

Abstract

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.

Access

Surface provides description only. Full text is available to ProQuest subscribers. Ask your Librarian for assistance.

http://libezproxy.syr.edu/login?url=http://proquest.umi.com/pqdweb?did=742476081&sid=2&Fmt=2&clientId=3739&RQT=309&VName=PQD

Link to Full Text

Share

COinS