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.

Performance Analysis and Design Aids (acm B.4.4), Requirements/Specifications (acm D.2.1), Software/Program Verification (acm D.2.4)
Specification and verification (program logics, model checking, etc.) (msc 68Q60)
Software Engineering [SEN]

Arts, T, & van Langevelde, I.A. (1999). Verifying a smart design of TCAP : a synergetic experience. Software Engineering [SEN]. CWI.