Verifying a Smart Design of TCAP. A Synergetic Experience. Software Engineering

摘要

An optimization of the SS No. 7 Transport Capabilities Procedures is verified by211u001especifying both the original and the optimized TCAP in (micrometer)CRL, 211u001egenerating transition systems for both using the (micrometer)CRL tool set, and 211u001echecking weak bisimulation equivalence of the two using the Caesar/Aldebaran tool 211u001eset, these steps being part of a iterative process of specification, refinement 211u001eand verification. As a result, the optimization design is debugged, a deeper 211u001eunderstanding of the protocol is gained, and the usability of the (micrometer)CRL 211u001etool set is evaluated. In conclusion, the design of an optimized TCAP indeed 211u001ebenefited from the verification reported here, and (micrometer)CRL and 211u001eCaesar/Aldebaran appeared to be a largely adequate combination for the 211u001everification at hand; however, since the characteristics of TCAP were not 211u001eexplicit from the start, and the tools used covered the functionality required 211u001enot perfectly, the verification required a good deal of human ingenuity and 211u001estamina.