Please use this identifier to cite or link to this item:
Title: Verifying and comparing finite state machines for systems that have distributed interfaces
Authors: Hierons, RM
Keywords: D2.4: software engineering/software/program verification;D2.5: software engineering/testing and debugging;Distributed systems;Distributed test architecture;Finite state machine
Issue Date: 2013
Publisher: Institute of Electrical and Electronics Engineers
Citation: IEEE Transactions on Computers, 62(8), 1673 - 1683, 2013
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 ⊆s and prove that it is undecidable whether N ⊆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 ⊆s M is decidable. We then consider implementation relation ⊆sk that concerns input sequences of length κ or less. If we place bounds on κ and the number of ports then we can decide N ⊆sk M in polynomial time but otherwise this problem is NP-hard.
ISSN: 0018-9340
Appears in Collections:Publications
Dept of Computer Science Research Papers

Files in This Item:
File Description SizeFormat 
distrib_conf_final.pdf175.81 kBUnknownView/Open

Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.