Equivalence Checking of TTCN-3 Test Case Behavior

Previous work has shown that refactoring can be used to improve the internal quality of TTCN-3 test cases. However, refactorings and their improper application are susceptible to introducing unintentional changes to the observable behavior of test cases. An approach to validate that refactorings and their application are indeed behavior preserving is proposed in this thesis. The original unrefactored and the refactored test cases will be checked for equivalent observable behavior. The approach is based on bisimulation, and is applied on the fly to manage the state-space explosion problem. A prototypical implementation of the proposed approach is presented briefly, along with selected examples to illustrate its application and prove its applicability.