Tagging make local testing of message-passing systems feasible

Abstract

The only practical way to test distributed message-passing systems is to use local testing. In this approach, used in formalisms such as concurrent TTCN-3, some components are replaced by test processes. Local testing consists of monitoring the interactions between these test processes and the rest of the system and comparing these observations with the specification, typically described in terms of message sequence charts. The main difficulty with this approach is that local observations can combine in unexpected ways to define implied scenarios not present in the original specification. Checking for implied scenarios is known to be undecidable for regular specifications, even if observations are made for all but one process at a time. We propose an approach where we append tags to the messages generated by the system under test. Our tags are generated in a uniform manner, without referring to or influencing the internal details of the underlying system. These enriched behaviours are then compared against a tagged version of the specification. Our main result is that detecting implied scenarios becomes decidable in the presence of tagging.