In: Proc. 10th International Conference on Multi-Media Modelling (MMM 2004), pages 323-328. January 2005. Brisbane, Australia.
Abstract: The Capability Exchange Signalling (CES) protocol is a sub-protocol of ITU-T Recommendation H.245, "Control protocol for multimedia communication". We are interested in verifying this protocol, including verification of its general properties such as absence of deadlocks and livelocks, and verification of the protocol against its service. In previous work, we have analysed the general properties of the CES protocol. In order to verify the protocol against its service, we need to generate the CES service language, which defines all the possible sequences of user observable events. We firstly create the CES service CPN model and then extract the language from the Occurrence Graph (OG) of the model. In the case of the CES service this is challenging because we wish to have a general result for arbitrary capacity of the network over which the CES protocol operates. To tackle this problem we introduced into the CPN model a parameter, l, representing the capacit y of the communication channel. We derived a recursive formula for the parameterized OG in terms of l. We treat this OG as a Finite State Automaton (FSA) by nominating acceptance states and apply FSA reduction algorithms to obtain a deterministic FSA that represents the CES service language. We have discovered a recursive formula in l for the CES service language. This paper introduces the CES service via its CPN model as necessary background and presents the final step of the proof of this finding.
Keywords: Multimedia Protocols; Formal Methods; Automata; Coloured Petri Nets; Recursive Service Language.