Formal specification and verification of the kernel functional unit of the OSI session layer protocol and service using CCS

Milica Barjaktarović, Shiu Kai Chin, Kamal Jabbour

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper describes an application of formal methods to protocol specification, validation and verification. Formal methods can be incorporated in protocol design and testing so that time and resources are saved on implementation, testing, and documentation. In this paper we show how formal methods can be used to write the control sequence, i.e. pseudo code, which can be formally tested using automated support. The formal specification serves as a blueprint for a correct implementation with desired properties.As a formal method we chose a process algebra called "plain" Calculus of Communicating Systems (CCS). Our specific objectives were to: 1) build a CCS model of the Kernel Functional Unit of OSI session layer service: 2) obtain a session protocol specification through stepwise refinement of the service specification; and 3) verify that the protocol specification satisfies the service specification. We achieved all of our objectives. Verification and validation were accomplished by using the CCS's model checker, the Edinburgh Concurrency Workbench (CWB). We chose plain CCS because of itssuccinct, abstract, and modular specifications, strong mathematical foundation which allows for formal reasoning and proofs, and existence of the automated support tool which supports temporal logic. The motivation for this work is: 1) testing the limits of CCS's succinct notation; 2) combining CCS and temporal logic; and 3) using a model-checker on a real-life example.

Original languageEnglish (US)
Title of host publicationProceedings of the 1996 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 1996
PublisherAssociation for Computing Machinery, Inc
Pages270-279
Number of pages10
ISBN (Electronic)0897917871, 9780897917872
DOIs
StatePublished - May 1 1996
Event1996 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 1996 - San Diego, United States
Duration: Jan 8 1996Jan 10 1996

Other

Other1996 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 1996
CountryUnited States
CitySan Diego
Period1/8/961/10/96

Keywords

  • communication protocols
  • formal methods
  • OSI
  • process algebra. CCS. automated support
  • Session Layer
  • specification
  • verification

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Formal specification and verification of the kernel functional unit of the OSI session layer protocol and service using CCS'. Together they form a unique fingerprint.

  • Cite this

    Barjaktarović, M., Chin, S. K., & Jabbour, K. (1996). Formal specification and verification of the kernel functional unit of the OSI session layer protocol and service using CCS. In Proceedings of the 1996 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 1996 (pp. 270-279). Association for Computing Machinery, Inc. https://doi.org/10.1145/229000.226325