This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Verifying and Comparing Finite State Machines for Systems that Have Distributed Interfaces
Aug. 2013 (vol. 62 no. 8)
pp. 1673-1683
Robert M. Hierons, Brunel University,Uxbridge
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, a local trace, is observed at each port. As a result the environment has reduced observational power: the set of local traces observed need not define the global trace that occurred. We consider the previously defined implementation relation $(\sqsubseteq_s)$ and prove that it is undecidable whether $(N \sqsubseteq_{s}M)$ and so it is also undecidable whether testing can distinguishing two states or FSMs. We also prove that a form of model-checking is undecidable when we have distributed observations and give conditions under which $(N \sqsubseteq_{s}M)$ is decidable. We then consider implementation relation $(\sqsubseteq_{s}^k)$ that concerns input sequences of length $(k)$ or less. 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.
Index Terms:
Automata,Controllability,Polynomials,Computer architecture,distributed test architecture,D2.4: software engineering/software/program verification,D2.5: software engineering/testing and debugging,distributed systems,finite state machine
Citation:
Robert M. Hierons, "Verifying and Comparing Finite State Machines for Systems that Have Distributed Interfaces," IEEE Transactions on Computers, vol. 62, no. 8, pp. 1673-1683, Aug. 2013, doi:10.1109/TC.2012.252
Usage of this product signifies your acceptance of the Terms of Use.