Correct Performance of Transaction Capabilities

The correctness of an optimisation of the Transport Capabilities Application Part of the Signalling System No. 7 is formalised as a branching bisimulation which is relaxed to allow certain actions to be executed in any order. It is demonstrated how this correctness can be checked by a combination of an automated test of branching bisimulation and a manual test of commutation. Using this approach, two bugs in the design were found and eliminated.

• Type: Conference
• Year: 2001
• Where: ACSD
• Authors: Thomas Arts, Izak van Langevelde
• Keywords: ACSD 2001, Branching Bisimulation, Capabilities Application Part, Correctness, Hardware