Subscribe
Issue No.08 - Aug. (2013 vol.62)
pp: 1673-1683
Robert M. Hierons , Brunel University,Uxbridge
ABSTRACT
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
REFERENCES
 [1] J. T. C. ISO/IEC JTC 1, International Standard ISO/IEC 9646-1. Information Technology - Open Systems Interconnection - Conformance Testing Methodology and Framework - Part 1: General Concepts, 1994. [2] O. Rafiq and L. Cacciari, "Coordination Algorithm for Distributed Testing," The J. Supercomputing, vol. 24, no. 2, pp. 203-211, 2003. [3] E.G. Cartaxo, P.D.L. Machado, and F.G.O. Neto, "On the Use of a Similarity Function for Test Case Selection in the Context of Model-Based Testing," Software Testing, Verification and Reliability, vol. 21, no. 2, pp. 75-100, 2011. [4] A. Cavalcanti and M.-C. Gaudel, "Testing for Refinement in Circus," Acta Informatica, vol. 48, no. 2, pp. 97-147, 2011. [5] W. Grieskamp, "Multi-Paradigmatic Model-Based Testing," Formal Approaches to Software Testing and Runtime Verification, vol. 4262, pp. 1-19, 2006. [6] J. Tretmans, "Model Based Testing with Labelled Transition Systems," Formal Methods and Testing, vol. 4949, pp. 1-38, 2008. [7] W. Grieskamp, N. Kicillof, K. Stobie, and V. Braberman, "Model-Based Quality Assurance of Protocol Documentation: Tools and Methodology," The J. Software Testing, Verification and Reliability, vol. 21, no. 1, pp. 55-71, 2011. [8] E.F. Moore, "Gedanken-Experiments," Automata Studies, Shannon and McCarthy, eds. Princeton Univ. Press, 1956. [9] M.C. Gaudel, "Testing can be Formal too," Proc. Sixth Int'l Joint Conf. CAAP/FASE Theory and Practice of Software Development (TAPSOFT '95), vol. 915, pp. 82-96, 1995. [10] R. Dssouli and G. von Bochmann, "Error Detection with Multiple Observers," Proc. Fifth Int'l Conf. Protocol Specification, Testing and Verification V, pp. 483-494, 1985. [11] R. Dssouli and G. von Bochmann, "Conformance Testing with Multiple Observers," Proc. Int'l Conf. Protocol Specification, Testing and Verification VI, pp. 217-229, 1986. [12] B. Sarikaya and G.v. Bochmann, "Synchronization and Specification Issues in Protocol Testing," IEEE Trans. Comm., vol. 32, no. 4, pp. 389-395, Apr. 1984. [13] H. Ural and C. Williams, "Constructing Checking Sequences for Distributed Testing," Formal Aspects of Computing, vol. 18, no. 1, pp. 84-101, 2006. [14] G. von Bochmann, S. Haar, C. Jard, and G.-V. Jourdan, "Testing Systems Specified as Partial Order Input/Output Automata," Proc. 20th IFIP TC 6/WG 6.1 Int'l Conf. Testing of Software and Communicating Systems (TestCom/FATES), vol. 5047, pp. 169-183, 2008. [15] R.M. Hierons, M.G. Merayo, and M. Núñez, "Implementation Relations and test Generation for Systems with Distributed Interfaces," Distributed Computing, vol. 25, no. 1, pp. 35-62, 2012. [16] R.M. Hierons, "Oracles for Distributed Testing," IEEE Trans. Software Eng., vol. 38, no. 3, pp. 629-641, May/June 2012. [17] R. Alur, K. Etessami, and M. Yannakakis, "Realizability and Verification of MSC Graphs," Theoretical Computer Science, vol. 331, no. 1, pp. 97-114, 2005. [18] R. Alur, C. Courcoubetis, and M. Yannakakis, "Distinguishing Tests for Nondeterministic and Probabilistic Machines," Proc. 27th ACM Symp. Theory of Computing, pp. 363-372. 1995, [19] A.V. Aho, A.T. Dahbura, D. Lee, and M.U. Uyar, "An Optimization Technique for Protocol Conformance Test Generation Based on UIO Sequences and Rural Chinese Postman Tours," IEEE Trans. Comm., vol. 39, no. 11, pp. 1604-1615, Nov. 1991. [20] T.S. Chow, "Testing Software Design Modeled by Finite State Machines," IEEE Trans. Software Eng., vol. TSE-4, pp. 178-187, May 1978. [21] A. Petrenko and N. Yevtushenko, "Testing from Partial Deterministic FSM Specifications," IEEE Trans. Computers, vol. 54, no. 9, pp. 1154-1165, Sept. 2005. [22] H. Ural, X. Wu, and F. Zhang, "On Minimizing the Lengths of Checking Sequences," IEEE Trans. Computers, vol. 46, no. 1, pp. 93-99, Jan. 1997. [23] R.M. Hierons, "Reaching and Distinguishing States of Distributed Systems," SIAM J. Computing, vol. 39, no. 8, pp. 3480-3500, 2010. [24] G. Luo, A. Petrenko, and G.v. Bochmann, "Selecting Test Sequences for Partially-Specified Nondeterministic Finite State Machines," Proc. Seventh IFIP Workshop Protocol Test Systems, pp. 95-110, Nov. 1994. [25] F. Werner and D. Faragó, "Correctness of Sensor Network Applications by Software Bounded Model Checking," Proc. 15th Int'l Conf. Formal Methods for Industrial Critical Systems (FMICS '10), vol. 6371, pp. 115-131, 2010. [26] Y. Jia and M. Harman, "An Analysis and Survey of the Development of Mutation Testing," IEEE Trans. Software Eng., vol. 37, no. 5, pp. 649-678, Sept./Oct. 2011. [27] M.O. Rabin and D. Scott, "Finite Automata and their Decision Problems," IBM J. Research and Development, vol. 3, no. 2, pp. 114-125, 1959. [28] B. Genest, A. Muscholl, H. Seidl, and M. Zeitoun, "Infinite-State High-Level MSCs: Model-Checking and Realizability," J. Computer and System Sciences, vol. 72, no. 4, pp. 617-647, 2006. [29] A. Bouajjani, A. Muscholl, and T. Touili, "Permutation Rewriting and Algorithmic Verification," Proc. 16th Symp. Logic in Computer Science (LICS '01), 2001. [30] R.M. Hierons, "Checking Experiments for Stream X-Machines," Theoretical Computer Science, vol. 411, no. 37, pp. 3372-3385, 2010. [31] V. Diekert and Y. Métivier, "Partial Commutation and Traces," Handbook of Formal Languages: Beyond Words, vol. 3, pp. 457-533, Springer, 1997. [32] K. CulikII and J. Karhumäki, "HDTOL Matching of Computations of Multitape Automata," Acta Informatica, vol. 27, no. 2, pp. 179-191, 1989. [33] T. Harju and J. Karhumäki, "The Equivalence Problem of Multitape Finite Automata," Theoretical Computer Science, vol. 78, no. 2, pp. 347-355, 1991. [34] M. Clerbout and M. Latteux, "Semi-Commutations," Information and Computation, vol. 73, no. 1, pp. 59-74, 1987. [35] A. Bertoni, G. Mauri, and N. Sabadini, "Equivalence and Membership Problems for Regular Trace Languages," Automata, Languages and Programming, vol. 140, pp. 61-71, 1982. [36] T.J. Schaefer, "The Complexity of Satisfiability Problems," Proc. 10th Ann. ACM Symp. Theory of Computing (STOC), pp. 216-226, 1978.