In: Farn Wang (Ed.): Lecture Notes in Computer Science, Vol. 3299: Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004, pages 483-486. Springer-Verlag, 2004.
Abstract: The Capability Exchange Signalling (CES) protocol is a control protocol for multimedia communications developed by the International Telecommunication Union (ITU). Our goal is to verify this protocol against the set of allowable sequences of service primitives (i.e. user observable events), known as the service language. Thus the first step to verify the CES protocol is to obtain the CES service language. By using automata reduction techniques, our approach is to extract the service language from the Occurrence Graph (OG) of the Coloured Petri Net (CPN) model for the protocol's service definition. The OG of a CPN model is a directed graph comprising all reachable states (nodes) and state changes (edges) of the model.