Verifying a smart design of TCAP : a synergetic experience

An optimisation of the SS No. 7 Transport Capabilities Procedures is verified by specifying both the original and the optimised {scriptsize sf TCAP in {scriptsize sf $mu$CRL, generating transition systems for both using the {scriptsize sf $mu$CRL tool set, and checking weak bisimulation equivalence of the two using the C{aesar/Ald'{ebaran tool set, these steps being part of a iterative process of specification, refinement and verification. As a result, the optimisation design is debugged, a deeper understanding of the protocol is gained, and the usability of the {scriptsize sf $mu$CRL tool set is evaluated. In conclusion, the design of an optimised {scriptsize sf TCAP indeed benefitted from the verification reported here, and {scriptsize sf $mu$CRL and C{aesar/Ald'{ebaran appeared to be a largely adequate combination for the verification at hand; however, since the characteristics of {scriptsize sf TCAP were not explicit from the start, and the tools used covered the functionality required not perfectly, the verification required a good deal of human ingenuity and stamina.