Formal specification and verification of OSI session layer protocol using CCS

This paper describes an application of formal methods to protocol specification, validation and verification. The chosen formal method is the Calculus of Communicating Systems (CCS), which is used to build a CCS model of the Open Systems Interconnection (OSI) Reference model session layer protocol and prove its inherent livelock using the CCS automated support.