maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2020-4-376-395mais-1431Research ArticleTheory of ComputingСинтез установочных последовательностей для автоматов с временными ограничениямиDeriving Homing Sequences for Finite State Machines with Timed Guardshttps://orcid.org/0000-0001-7705-7214ТвардовскийАлександр СергеевичTvardovskiiAleksandr Sergeevich

Кандидат физико-математических наук

PhD

tvardal@mail.ruhttps://orcid.org/0000-0002-4006-1161ЕвтушенкоНина ВладимировнаYevtushenkoNina Vladimirovna

Доктор технических наук, профессор

Doctor of technical sciences, professor

evtushenko@ispras.ruНациональный исследовательский Томский Государственный университетРоссияNational Research Tomsk State UniversityRussian FederationИнститут системного программирования РАН; Национальный исследовательский университет «Высшая школа экономики»РоссияIvannikov Institute for System Programming of the RAS; National Research University Higher School of EconomicsRussian Federation202018122020274376395Copyright © Твардовский А.С., Евтушенко Н.В., 20202020Твардовский А.С., Евтушенко Н.В.Tvardovskii A.S., Yevtushenko N.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1431

Идентификация состояний является хорошо известной задачей теории конечных автоматов, и установочные последовательности, которые позволяют идентифицировать текущее состояние конечного автомата, широко используются в областях тестирования и верификации программного и аппаратного обеспечения. Для автоматов различных классов, полностью определенных и частичных, детерминированных и недетерминированных, установлены необходимые и достаточные условия существования безусловных и адаптивных установочных последовательностей и предложены алгоритмы их синтеза, если такая последовательность существует. В настоящее время при верификации и тестировании программного и аппаратного обеспечения необходимо учитывать временные аспекты, что приводит к расширению автоматных моделей временными переменными. В настоящей работе мы исследуем задачи проверки существования и синтеза безусловных и адаптивных установочных последовательностей для автоматов с временными ограничениями и показываем, что оценки на длину таких последовательностей совпадают с оценками для классических конечных автоматов. Предлагаемый подход основан на использовании конечно-автоматной абстракции временного автомата, то есть описании временного автомата соответствующим конечным автоматом, который сохраняет свойства временного автомата относительно установочных последовательностей.

State identification is the well-known problem in the theory of Finite State Machines (FSM) where homing sequences (HS) are used for the identification of a current FSM state, and this fact is widely used in the area of software and hardware testing and verification. For various kinds of FSMs, such as partial, complete, deterministic, non-deterministic, there exist sufficient and necessary conditions for the existence ofpreset and adaptive HS and algorithms for their derivation. Nowadays timed aspects become very important for hardware and software systems and for this reason classical FSMs are extended by clock variables. In this work, we address the problem of checking the existence and derivation of homing sequences for FSMs with timed guards and show that the length estimation for timed homing sequence coincides with that for untimed FSM. The investigation is based on the FSM abstraction of a Timed FSM, i.e. on a classical FSM which describes behavior of corresponding TFSM and inherits some of its properties. When solving state identification problems for timed FSMs, the existing FSM abstraction is properly optimized.

конечный автоматвременные ограниченияконечно-автоматная абстракцияустановочная последовательностьFinite State Machinetimed guardsFSM abstractionhoming sequenceРФФИ, проект № 19-07-00327RFBR, project 19-07-00327ReferencesA. Gill, Introduction to the Theory of Finite-State Machines. McGraw-Hill, 1962.A. Gill, Introduction to the Theory of Finite-State Machines. McGraw-Hill, 1962.D. Lee and M. Yannakakis, “Testing finite state machines: state identification and verification”, IEEE Transactions on Computers, vol. 43, no. 3, pp. 306-320, 1994.D. Lee and M. Yannakakis, “Testing finite state machines: state identification and verification”, IEEE Transactions on Computers, vol. 43, no. 3, pp. 306-320, 1994.T. N. Hibbard, “Least upper bounds on minimal terminal state experiments for two classes of sequential machines”, Journal of the ACM, vol. 8, no. 4, pp. 601-612, 1961.T. N. Hibbard, “Least upper bounds on minimal terminal state experiments for two classes of sequential machines”, Journal of the ACM, vol. 8, no. 4, pp. 601-612, 1961.Z. Kohavi, Switching and Finite Automata Theory. McGraw-Hill, 1978.Z. Kohavi, Switching and Finite Automata Theory. McGraw-Hill, 1978.P. Starke, Abstract Automata. American Elsevier, 1972.P. Starke, Abstract Automata. American Elsevier, 1972.G. Bochmann and A. Petrenko, “Protocol testing: review of methods and relevance for software testing”, in In Proc. of International Symposium on Software Testing and Analysis, 1994, pp. 109-124.G. Bochmann and A. Petrenko, “Protocol testing: review of methods and relevance for software testing”, in In Proc. of International Symposium on Software Testing and Analysis, 1994, pp. 109-124.G.-V. Jourdan, H. Ural, and H. Yenigun, “Reduced checking sequences using unreliable reset”, Information Processing Letters, vol. 115, no. 5, pp. 532-535, 2015.G.-V. Jourdan, H. Ural, and H. Yenigun, “Reduced checking sequences using unreliable reset”, Information Processing Letters, vol. 115, no. 5, pp. 532-535, 2015.N. Kushik, J. Lopez, A. Cavalli, and N. Yevtushenko, “Improving Protocol Passive Testing through ”Gedanken” Experiments with Finite State Machines”, in IEEE International Conference on Software Qality, Reliability and Security, 2016, pp. 315-322.N. Kushik, J. Lopez, A. Cavalli, and N. Yevtushenko, “Improving Protocol Passive Testing through ”Gedanken” Experiments with Finite State Machines”, in IEEE International Conference on Software Qality, Reliability and Security, 2016, pp. 315-322.F. Hennie, “Fault-detecting experiments for sequential circuits”, in Proceedings of Fifth Annual Symposium on Circuit Theory and Logical Design, 1965, pp. 95-110.F. Hennie, “Fault-detecting experiments for sequential circuits”, in Proceedings of Fifth Annual Symposium on Circuit Theory and Logical Design, 1965, pp. 95-110.T. S. Chow, “Testing software design modeled by finite-state machines”, IEEE Transactions on Software Engineering, vol. 4, no. 3, pp. 178-187, 1978.T. S. Chow, “Testing software design modeled by finite-state machines”, IEEE Transactions on Software Engineering, vol. 4, no. 3, pp. 178-187, 1978.H.-E. Wang, K.-H. Tu, J.-H. R. Jiang, and N. Kushik, “Homing Sequence Derivation with Quantified Boolean Satisfiability”, in Testing Software and Systems, ser. LNCS, vol. 10533, 2017, pp. 230-242.H.-E. Wang, K.-H. Tu, J.-H. R. Jiang, and N. Kushik, “Homing Sequence Derivation with Quantified Boolean Satisfiability”, in Testing Software and Systems, ser. LNCS, vol. 10533, 2017, pp. 230-242.H. Yenigun, N. Yevtushenko, N. Kushik, and J. Lopez, “The effect of partiality and adaptivity on the complexity of FSM state identification problems”, Trudy ISP RAN/Proceedings ISP RAS, vol. 30, no. 1, pp. 7-24, 2018.H. Yenigun, N. Yevtushenko, N. Kushik, and J. Lopez, “The effect of partiality and adaptivity on the complexity of FSM state identification problems”, Trudy ISP RAN/Proceedings ISP RAS, vol. 30, no. 1, pp. 7-24, 2018.N. Kushik and N. Yevtushenko, “On the Length of Homing Sequences for Nondeterministic Finite State Machines”, in Implementation and Application of Automata, ser. LNCS, vol. 7982, Springer, 2013, pp. 220-231.N. Kushik and N. Yevtushenko, “On the Length of Homing Sequences for Nondeterministic Finite State Machines”, in Implementation and Application of Automata, ser. LNCS, vol. 7982, Springer, 2013, pp. 220-231.S. Sandberg, “Homing and Synchronizing Sequences”, in Model-Based Testing of Reactive Systems, ser. LNCS, vol. 3472, Springer, 2005, pp. 5-33.S. Sandberg, “Homing and Synchronizing Sequences”, in Model-Based Testing of Reactive Systems, ser. LNCS, vol. 3472, Springer, 2005, pp. 5-33.E. Bayse, A. R. Cavalli, M. Nu´nez, and Zaıdi, “A passive testing approach based on invariants: application to the WAP”, Computer Networks, vol. 48, no. 2, pp. 247-266, 2005.E. Bayse, A. R. Cavalli, M. Nu´nez, and Zaıdi, “A passive testing approach based on invariants: application to the WAP”, Computer Networks, vol. 48, no. 2, pp. 247-266, 2005.N. Kushik, K. El-Fakih, and N. Yevtushenko, “Preset and Adaptive Homing Experiments for Nondeterministic Finite State Machines”, in Implementation and Application of Automata, ser. LNCS, vol. 6807, Springer, 2011, pp. 215-224.N. Kushik, K. El-Fakih, and N. Yevtushenko, “Preset and Adaptive Homing Experiments for Nondeterministic Finite State Machines”, in Implementation and Application of Automata, ser. LNCS, vol. 6807, Springer, 2011, pp. 215-224.N. Kushik, K. El-Fakih, and N. Yevtushenko, “Adaptive Homing and Distinguishing Experiments for Nondeterministic Finite State Machines”, in Testing Software and Systems, ser. LNCS, vol. 8254, Springer, 2013, pp. 33-48.N. Kushik, K. El-Fakih, and N. Yevtushenko, “Adaptive Homing and Distinguishing Experiments for Nondeterministic Finite State Machines”, in Testing Software and Systems, ser. LNCS, vol. 8254, Springer, 2013, pp. 33-48.N. Kushik and H. Yenigun, “Heuristics for Deriving Adaptive Homing and Distinguishing Sequences for Nondeterministic Finite State Machines”, in Testing Software and Systems, ser. LNCS, vol. 9447, Springer, 2015, pp. 243-248.N. Kushik and H. Yenigun, “Heuristics for Deriving Adaptive Homing and Distinguishing Sequences for Nondeterministic Finite State Machines”, in Testing Software and Systems, ser. LNCS, vol. 9447, Springer, 2015, pp. 243-248.H. Yenigun, N. Yevtushenko, and N. Kushik, “The complexity of checking the existence and derivation of adaptive synchronizing experiments for deterministic FSMs”, Information Processing Letters, vol. 127, pp. 49-53, 2017.H. Yenigun, N. Yevtushenko, and N. Kushik, “The complexity of checking the existence and derivation of adaptive synchronizing experiments for deterministic FSMs”, Information Processing Letters, vol. 127, pp. 49-53, 2017.M. Krichen and S. Tripakis, “Conformance testing for real-time systems”, Formal Methods in System Design, vol. 34, no. 3, pp. 238-304, 2009.M. Krichen and S. Tripakis, “Conformance testing for real-time systems”, Formal Methods in System Design, vol. 34, no. 3, pp. 238-304, 2009.K. El-Fakih, N. Yevtushenko, and H. Fouchal, “Testing timed finite state machines with guaranteed fault coverage”, in Proc. of the 21st IFIP WG 6.1 Int. Conf, on Testing of Software and Communication Systems and 9th Int. FATES Workshop, 2009, pp. 66-80.K. El-Fakih, N. Yevtushenko, and H. Fouchal, “Testing timed finite state machines with guaranteed fault coverage”, in Proc. of the 21st IFIP WG 6.1 Int. Conf, on Testing of Software and Communication Systems and 9th Int. FATES Workshop, 2009, pp. 66-80.M. Merayo, M. Nunez, and I. Rodriguez, “Formal testing from timed finite state machines”, Computer Networks: The International Journal of Computer and Telecommunications Networking, vol. 52, no. 2, pp. 432-460, 2008.M. Merayo, M. Nunez, and I. Rodriguez, “Formal testing from timed finite state machines”, Computer Networks: The International Journal of Computer and Telecommunications Networking, vol. 52, no. 2, pp. 432-460, 2008.D. Bresolin, K. El-Fakih, T. Villa, and N. Yevtushenko, “Deterministic timed finite state machines: Equivalence checking and expressive power”, in International conference GANDALF, 2014, pp. 203-216.D. Bresolin, K. El-Fakih, T. Villa, and N. Yevtushenko, “Deterministic timed finite state machines: Equivalence checking and expressive power”, in International conference GANDALF, 2014, pp. 203-216.M. Gromov, K. El-Fakih, N. Shabaldina, and N. Yevtushenko, “Distinguishing non-deterministic timed finite state machines”, in In Formal Techniques for Distributed Systems, ser. LNCS, vol. 5522, Springer, 2009, pp. 137-151.M. Gromov, K. El-Fakih, N. Shabaldina, and N. Yevtushenko, “Distinguishing non-deterministic timed finite state machines”, in In Formal Techniques for Distributed Systems, ser. LNCS, vol. 5522, Springer, 2009, pp. 137-151.K. Tvardovskii A.S.and El-Fakih, M. Gromov, and N. Yevtushenko, “Testing Timed Nondeterministic Finite State Machines withthe Guaranteed Fault Coverage”, Automatic Control and Computer Sciences, vol. 51, no. 7, pp. 724-730, 2017.K. Tvardovskii A.S.and El-Fakih, M. Gromov, and N. Yevtushenko, “Testing Timed Nondeterministic Finite State Machines withthe Guaranteed Fault Coverage”, Automatic Control and Computer Sciences, vol. 51, no. 7, pp. 724-730, 2017.A. Tvardovskii and N. Yevtushenko, “Deriving homing sequences for Finite State Machines with timed guards”, System Informatics, vol. 17, pp. 1-10, 2020.A. Tvardovskii and N. Yevtushenko, “Deriving homing sequences for Finite State Machines with timed guards”, System Informatics, vol. 17, pp. 1-10, 2020.J. Hartmanis and R. Stearns, Algebraic structure theory ofsequential machines. Prentice-Hall, 1966.J. Hartmanis and R. Stearns, Algebraic structure theory ofsequential machines. Prentice-Hall, 1966.E. Vinarskii, A. Tvardovskii, L. Evtushenko, and N. Yevtushenko, “Deriving adaptive homing sequences for weakly initialized nondeterministic FSMs”, 2019, pp. 1-5.E. Vinarskii, A. Tvardovskii, L. Evtushenko, and N. Yevtushenko, “Deriving adaptive homing sequences for weakly initialized nondeterministic FSMs”, 2019, pp. 1-5.N. Yevtushenko, V. Kuliamin, and N. Kushik, “Evaluating the Complexity of Deriving Adaptive Homing, Synchronizing and Distinguishing Sequences for Nondeterministic FSMs”, in Testing Software and Systems, ser. LNCS, vol. 11812, Springer, 2019, pp. 86-103.N. Yevtushenko, V. Kuliamin, and N. Kushik, “Evaluating the Complexity of Deriving Adaptive Homing, Synchronizing and Distinguishing Sequences for Nondeterministic FSMs”, in Testing Software and Systems, ser. LNCS, vol. 11812, Springer, 2019, pp. 86-103.E. Vinarskii and N. Yevtushenko, “Evaluating Length of a Shortest Adaptive Homing Sequence for Weakly Initialized FSMs”, 2020, pp. 1-5.E. Vinarskii and N. Yevtushenko, “Evaluating Length of a Shortest Adaptive Homing Sequence for Weakly Initialized FSMs”, 2020, pp. 1-5.N. Kushik and N. Yevtushenko, “Adaptive Homing is in P”, Electronic Proceedings in Theoretical ComputerScience, vol. 180, pp. 73-78, 2015.N. Kushik and N. Yevtushenko, “Adaptive Homing is in P”, Electronic Proceedings in Theoretical ComputerScience, vol. 180, pp. 73-78, 2015.

The authors declare that there are no conflicts of interest present.