FSM abstraction based method for deriving test suites with guaranteed fault coverage against nondeterministic Finite State Machines with timed guards and timeouts

Finite State Machine (FSM) based approaches are widely used for deriving tests with guaranteed fault coverage for discrete event systems and as the behavior of many nowadays information and control systems depends on time, classical FSMs are extended by clock variables. Moreover, optionality in the real system’s specifications motivates the studying test derivation against models with the nondeterministic behavior. In this paper, we adapt classical FSM based test derivation methods for nondeterministic FSMs with timed guards and timeouts (TFSMs). We show that unlike classical FSM conformance relation, the check cannot be reduced to checking the correspondence between TFSMs transitions and this violates the main principle of FSM based test derivation methods. Respectively, a proposed approach and the appropriate fault model are based on the FSM abstraction of the given TFSM specification that is used to adequately describe the behavior of a TFSM. The fault domain contains TFSMs with the known upper boundary on the number of FSM abstraction states and allows to avoid explicit enumeration of implementations under test. We study properties of the FSM abstraction for a nondeterministic TFSM and justify that the use of an FSM abstraction allows to adapt classical FSM based test derivation methods when deriving tests with guaranteed fault coverage for TFSMs. A method is proposed for deriving a complete test suite for a complete possibly nondeterministic TFSM when an implementation under test is a deterministic complete TFSM.

Finite State Machine, timeout, timed guard, nondeterministic Timed Finite State Machine, test derivation, fault coverage

1. Gill A. Introduction to the Theory of Finite-State Machines, McGraw-Hill, 1962, 272 p. / Гилл А. Введение в теорию конечных автоматов. Наука, 1966, 272 стр.

2. Chow T.S. Test design modeled by finite-state machines. IEEE Transactions on Software Engineering, vol. 4, no. 3, 1978,pp. 178–187.

3. Dorofeeva R., El-Fakih K., Maag S., Cavalli A., Yevtushenko N. FSM-based conformance testing methods: A survey annotated with experimental evaluation. Information and Software Technology, vol. 52, issue 12, 2010, pp. 1286–1297.

4. Hierons R.M., Merayo M.G., Nunez M. Testing from a Stochastic Timed System with a Fault Model. Journal of Logic and Algebraic Programming, vol. 72, no. 8, 2009, pp. 98–115.

5. Krichen M. and Tripakis S. Conformance testing for real-time systems. Formal Methods in System Design, vol. 34, no. 3, 2009, pp. 238–304.

6. Petrenko A., Yevtushenko N. Conformance tests as checking experiments for partial nondeterministic FSM. Lecture Notes in Computer Science, vol. 3997, 2006, pp. 118–133.

7. Tvardovskii A.S., Yevtushenko N.V. Deriving adaptive distinguishing sequences for Finite State Machines. Trudy ISP RAN/Proc. ISP RAS, vol. 30, issue 4, 2018, pp. 139–154 (in Russian). DOI: 10.15514/ISPRAS-2018-30(4)-9 / Твардовский А.С., Евтушенко Н.В. К синтезу адаптивных различающих последовательностей для конечных автоматов. Труды ИСП РАН, том 30, вып. 4, 2018, стр. 139–154.

8. Alur R. and Dill D.L. A theory of timed automata. Theoretical Computer Science, vol. 126, issue 2, 1994, pp. 183–235.

9. Springintveld J., Vaandrager F., and D’Argenio P. Testing timed automata. Theoretical Computer Science, vol. 254, no. 1–2, 2001, pp. 225–257.

10. El-Fakih K., Yevtushenko N., and Fouchal H., Testing timed finite state machines with guaranteed fault coverage. In Proc. of the 21st IFIP WG 6.1 International Conference on Testing of Software and Communication Systems and 9th International FATES Workshop, 2009, pp. 66–80.

11. Merayo M.G., Nunez M., and Rodriguez I. Formal testing from timed finite state machines. Computer Networks, vol. 52, issue 2, 2008, pp. 432–460.

12. Bresolin D., El-Fakih K., Villa T., and Yevtushenko N. Deterministic timed finite state machines: Equivalence checking and expressive power. In Proc. of the 5th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2014), 2014, pp. 203–216.

13. Zhigulin M., Yevtushenko N., Maag S., Cavalli A. FSM-Based Test Derivation Strategies for Systems with Time-Outs. In Proc. of the 11th International Conference on Quality Software, 2011, pp. 141–150.

14. En-Nouaary A., Dssouli R., Khendek F. Timed Wp-Method: Testing Real-Time Systems. IEEE Transactions on Software Engineering, vol. 28, issue 11, 2002, pp. 1023–1038.

15. Tvardovskii A., El-Fakih K, Yevtushenko N. Deriving Tests with Guaranteed Fault Coverage for Finite State Machines with Timeouts. Lecture Notes in Computer Science, vol. 11146, 2018, pp. 149–154.

16. Starke P. Abstract Automata. North-Holland Publishing Company, 1972, 419 p.

17. Villa T., Kam T., Brayton R.K., Sandgiovanni-Vincentelli A. Synthesis of Finite State machines: Logic Optimization, Springer, 1997, 381 p.

18. Lee D., Yannakakis M. Principles and methods of testing finite state machines - a survey. Proceedings of the IEEE, vol. 84, issue 8, 1996, pp. 1090–1123.

19. Yevtushenko N., El-Fakih K., and Ermakov A., On-the-fly construction of adaptive checking sequences for testing deterministic implementations of nondeterministic specifications. Lecture Notes in Computer Science, vol. 9976, 2016, pp. 139–152.

20. Tvardovskii A.S., Gromov M.L., El-Fakih Khaled, Yevtushenko N.V. Testing Timed Nondeterministic Finite State Machines with the Guaranteed Fault Coverage. Automatic Control and Computer Sciences, vol. 51, № 7, 2017, pp. 724–730.

21. Tvardovskii A., Vinarskii E. Yevtushenko N. Experimental Evaluation of Timed Finite State Machine Based Test Derivation. In Proc. of the International Conference of Young Specialists on Micro/Nanotechnologies and Electron Devices, 2019, pp. 102–107.

22.