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

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.

REFERENCES

• Aldw92: J. Aldwinckle, R. Nagarajan, G. Birtwistle, An lnt;vductzon to Modal Lo#zc and its Appltcattons on the Concurrency Workbench. Research Report. No.92/467/05, Dept. of Computer Science, Tile University of Calgary, February 1992
• Azco92: A. Azcorra, J. Queniada, J. Manas, "LOTOS Tool Survey". DIT-UPM report,, number R/I.2.3- UPM/i, Sel)tember 1992. A sumnlary of the report. was published in the LOTOS News, K. Turner (editor), Lotos-NA List ([e-mail]), Issue 0, August 1993.
• Barj95: Milica Barjaktarovic, Formal specification and verification of the osi session layer using the calculus of communicating systems (ccs), 1995
• Barj95': Formal specification and verification of communication protocols using automated tools, Proceedings of the 1st International Conference on Engineering of Complex Computer Systems, p.246, November 06-10, 1995
• Barj94: M. Barjaktarovi~, S.K. Chin, K. Jabbour, "Deep Embedding of CCS in Larch Using Penelope". New York State Center for Advanced Technology in Computer Applications and Software Engineering (CASE) Technical Report no.9411, Syracuse University, December 1994.
• Barj93: m. BarjaktaroviS. SK. Chin, K. Jabbour. Formal Specification and Verification of 0$I Session Layer Using CUS. CASE Center Technical Report. 9300 series, Syracuse University, Summer 1993.
• Birt92: G. Birtwistle, J. Aldwinckle, R. Nagarajan. at.all., Vanilla CCS- Part I: Specifying Systems. and Part H: Process Logic. Dept. of Computer Science. The University of Calgary, May 1992.
• Birt92': G. Birtwistle, J. Aldwinckle, Y. Liu. K.Stevens. Workshop Notes: CCS with Applications to Asynchronous Systems. Dept. of Computer Science, The University of Calgary. October 1992.
• Boch90: Gregor Bochmann, Protocol specification for OSI, Computer Networks and ISDN Systems, v.18 n.3, p.167-184, April 1990 [doi>10.1016/0169-7552(90)90132-C]
• Clev93: Rance Cleaveland , Joachim Parrow , Bernhard Steffen, The concurrency workbench: a semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.36-72, Jan. 1993 [doi>10.1145/151646.151648]
• Hoar85: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• ISO8326: Int. erllational Organization for Standardization, "Basic Connection Oriented Session Session Definition", ISO8326 standard, 1987.
• ISO8327: International Organization for Standardization, "Basic Connection Oriented Session Protocol Definition", iSO8327 standard, 1987.
• ISO8807: International Organization for Standardization, Information Processing Systems- Open Systems Interconnection- LOTOS- A formal description Technique Based on the Temporal Ordemng of Observational Behavzor. International Standard ISO 8807, ISO, 1989.
• Kirk94: C.E. Kirkwood, l&'rification of LOTOS Specification Using Term Rewr,tzng techniques. Ph.D. thesis, Department of Computer Science, University of Glasgow, June 1994.
• Moll94: F. Moller, P. Stevens, The Edinburgh Concurrency Workbench O,ers,on 7.0). Dept. of Computer Science, University of Edinburgh, December 1994.
• Miln89: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• Parr88: J. Parrow, "Verifying a CSMA/CD protocol with CCS". Protocol ..qpec~ficatlon. Testing and l krification I/VII, 1988, pp.373-384.
• Rudi88: H. Rudin, "Protocol Engineering: A Critical Assessment". Protocol Specification, Testing and verification VIii, 1988.
• Tane88: A. S. Tanenbaum, Computer networks, Prentice-Hall, Inc., Upper Saddle River, NJ, 1988
• Yoel91: M. Yoeli, "Temporal Logic". Formal Verification of Hardware Design, iEEE Computer Society Press Tutorial, 1991, pp. 159-16.5.
• Wing90: Jeannette M. Wing, A Specifier's Introduction to Formal Methods, Computer, v.23 n.9, p.8-23, September 1990 [doi>10.1109/2.58215]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

General Terms:
Design, Verification