engleski

Verifying Multiparty Call in ATM UNI Signalling Protocol

This paper presents formal specification and verification of the multiparty call in ATM UNI signalling protocol. The protocol specification is written in the CCS process algebra (Calculus of Communicating Systems). The verification is done by using the NCSU-Concurrency Workbench. Due to complexity of the protocol, the model is decomposed on three components. The protocol verification is done by using the model-checking feature of the Workbench. Each component of the protocol is checked for safety and liveness properties using the temporal CTL (Computation Tree Logic) and the modal mu-calculus logic.

formal specification, model checking, verification, ATM signalling protocol, process algebra

nije evidentirano