Paper detail

Checking Finite State Machine Conformance when there are Distributed Observations

This paper concerns state-based systems that interact with their environment at physically distributed interfaces, called ports. When such a system is used a projection of the global trace, called a local trace, is observed at each port. This leads to the environment having reduced observational power: the set of local traces observed need not uniquely define the global trace that occurred. We consider the previously defined implementation relation $\sqsubseteq_s$ and start by investigating the problem of defining a language ${\mathcal {\tilde L}} (M)$ for a multi-port finite state machine (FSM) $M$ such that $N \sqsubseteq_s M$ if and only if every global trace of $N$ is in ${\mathcal {\tilde L}} (M)$. The motivation is that if we can produce such a language ${\mathcal {\tilde L}} (M)$ then this can potentially be used to inform development and testing. We show that ${\mathcal {\tilde L}} (M)$ can be uniquely defined but need not be regular. We then prove that it is generally undecidable whether $N \sqsubseteq_s M$, a consequence of this result being that it is undecidable whether there is a test case that is capable of distinguishing two states or two multi-port FSM in distributed testing. This result complements a previous result that it is undecidable whether there is a test case that is guaranteed to distinguish two states or multi-port FSMs. We also give some conditions under which $N \sqsubseteq_s M$ is decidable. We then consider the implementation relation $\sqsubseteq_s^k$ that only concerns input sequences of length $k$ or less. Naturally, given FSMs $N$ and $M$ it is decidable whether $N \sqsubseteq_s^k M$ since only a finite set of traces is relevant. We prove that if we place bounds on $k$ and the number of ports then we can decide $N \sqsubseteq_s^k M$ in polynomial time but otherwise this problem is NP-hard.