Correctly slicing extended finite state machines. (English) Zbl 1440.68149

Di Pierro, Alessandra (ed.) et al., From lambda calculus to cybersecurity through program analysis. Essays dedicated to Chris Hankin on the occasion of his retirement. Cham: Springer. Lect. Notes Comput. Sci. 12065, 149-197 (2020).
Summary: We consider slicing extended finite state machines. Extended finite state machines (EFSMs) combine a finite state machine with a store and can model a range of computational phenomena, from high-level software to cyber-physical systems. EFSMs are essentially interactive, possibly non-terminating or with multiple exit states and may be nondeterministic, so standard techniques for slicing, developed for control flow graphs of programs with a functional semantics, are not immediately applicable.
This paper addresses the various aspects of correctness for slicing of EFSMs, and provides syntactic criteria that we prove are sufficient for our proposed notions of semantic correctness. The syntactic criteria are based on the “weak commitment” and “strong commitment” properties highlighted by S. Danicic et al. [Theor. Comput. Sci. 412, No. 49, 6809–6842 (2011; Zbl 1231.68179)]. We provide polynomial-time algorithms to compute the least sets satisfying each of these two properties. We have conducted experiments using widely-studied benchmark and industrial EFSMs that compare our slicing algorithms with those using existing definitions of control dependence. We found that our algorithms produce the smallest average slices sizes, 21% of the original EFSMs when “weak commitment” is sufficient and 58% when “strong commitment” is needed (to preserve termination properties).
For the entire collection see [Zbl 1435.68026].


68Q45 Formal languages and automata
68Q55 Semantics in the theory of computing


Zbl 1231.68179
Full Text: DOI


[1] Amtoft, T.: Slicing for modern program structures: a theory for eliminating irrelevant loops. Inf. Process. Lett. 106(2), 45-51 (2008). https://doi.org/10.1016/j.ipl.2007.10.002 · Zbl 1186.68120
[2] Androutsopoulos, K., Clark, D., Harman, M., Hierons, R.M., Li, Z., Tratt, L.: Amorphous slicing of extended finite state machines. IEEE Trans. Softw. Eng. 39(7), 892-909 (2013)
[3] Androutsopoulos, K., Clark, D., Harman, M., Krinke, J., Tratt, L.: State-based model slicing: a survey. ACM Comput. Surv. 45(4), 53:1-53:36 (2013)
[4] Androutsopoulos, K., Clark, D., Harman, M., Li, Z., Tratt, L.: Control dependence for extended finite state machines. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 216-230. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00593-0_15
[5] Androutsopoulos, K., Gold, N., Harman, M., Li, Z., Tratt, L.: A theoretical and empirical study of EFSM dependence. In: 25th IEEE International Conference on Software Maintenance (ICSM 2009), Edmonton, Alberta, Canada, 20-26 September 2009, pp. 287-296. IEEE Computer Society (2009)
[6] Ball, T., Horwitz, S.: Slicing programs with arbitrary control-flow. In: Fritzson, P.A. (ed.) AADEBUG 1993. LNCS, vol. 749, pp. 206-222. Springer, Heidelberg (1993). https://doi.org/10.1007/BFb0019410
[7] Blazy, S., Maroneze, A., Pichardie, D.: Verified validation of program slicing. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, pp. 109-117. ACM, New York (2015). https://doi.org/10.1145/2676724.2693169. http://doi.acm.org/10.1145/2676724.2693169
[8] Bourhfir, C., Dssouli, R., Aboulhamid, E., Rico, N.: Automatic executable test case generation for extended finite state machine protocols. In: Kim, M., Kang, S., Hong, K. (eds.) Testing of Communicating Systems. ITIFIP, pp. 75-90. Springer, Boston, MA (1997). https://doi.org/10.1007/978-0-387-35198-8_6
[9] Danicic, S., Barraclough, R.W., Harman, M., Howroyd, J.D., Kiss, A., Laurence, M.R.: A unifying theory of control dependence and its application to arbitrary program structures. Theoret. Comput. Sci. 412(49), 6809-6842 (2011) · Zbl 1231.68179
[10] Derler, P., Lee, E.A., Sangiovanni-Vincentelli, A.L.: Modeling cyber-physical systems. Proc. IEEE 100(1), 13-28 (2012). https://doi.org/10.1109/JPROC.2011.2160929
[11] Hafemann Fragal, V., Simao, A., Mousavi, M.R.: Validated test models for software product lines: featured finite state machines. In: Kouchnarenko, O., Khosravi, R. (eds.) FACS 2016. LNCS, vol. 10231, pp. 210-227. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57666-4_13
[12] Ganapathy, V., Ramesh, S.: Slicing synchronous reactive programs. Electron. Notes Theoret. Comput. Sci. 65(5), 50-64 (2002). SLAP 2002, Synchronous Languages, Applications, and Programming (Satellite Event of ETAPS 2002)
[13] Gold, N.E., Binkley, D., Harman, M., Islam, S., Krinke, J., Yoo, S.: Generalized observational slicing for tree-represented modelling languages. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, pp. 547-558. ACM, New York (2017)
[14] Hall, M., McMinn, P., Walkinshaw, N.: Superstate identification for state machines using search-based clustering. In: Pelikan, M., Branke, J. (eds.) Proceedings of the 12th Annual Conference on Genetic and Evolutionary Computation (GECCO 2010), pp. 1381-1388. ACM (2010)
[15] Harel, D., Politi, M.: Modeling Reactive Systems with Statecharts: The Statemate Approach, 1st edn. McGraw-Hill Inc., New York (1998)
[16] Hatcliff, J., Corbett, J., Dwyer, M., Sokolowski, S., Zheng, H.: A formal study of slicing for multi-threaded programs with JVM concurrency primitives. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 1-18. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48294-6_1
[17] Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. High.-Order Symb. Comput. 13(4), 315-353 (2000) · Zbl 0972.68021
[18] Ilie, L., Yu, S.: Reducing NFAs by invariant equivalences. Theoret. Comput. Sci. 306(1-3), 373-390 (2003) · Zbl 1059.68064
[19] Kamischke, J., Lochau, M., Baller, H.: Conditioned model slicing of feature-annotated state machines. In: Proceedings of the 4th International Workshop on Feature-Oriented Software Development, FOSD 2012, pp. 9-16. ACM, New York (2012)
[20] Korel, B., Singh, I., Tahat, L., Vaysburg, B.: Slicing of state-based models. In: IEEE International Conference on Software Maintenance (ICSM 2003), pp. 34-43. IEEE Computer Society Press, Los Alamitos, California, USA, September 2003 (2003)
[21] Labbé, S., Gallois, J.: Slicing communicating automata specifications: polynomial algorithms for model reduction. Form. Asp. Comput. 20(6), 563-595 (2008). https://doi.org/10.1007/s00165-008-0086-3 · Zbl 1163.68028
[22] Léchenet, J.-C., Kosmatov, N., Le Gall, P.: Fast computation of arbitrary control dependencies. In: Russo, A., Schürr, A. (eds.) FASE 2018. LNCS, vol. 10802, pp. 207-224. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89363-1_12
[23] Lity, S., Morbach, T., Thüm, T., Schaefer, I.: Applying incremental model slicing to product-line regression testing. In: Kapitsaki, G.M., Santana de Almeida, E. (eds.) ICSR 2016. LNCS, vol. 9679, pp. 3-19. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-35122-3_1
[24] Marwedel, P.: Embedded and cyber-physical systems in a nutshell. DAC.COM Knowl. Cent. Article no. 20 (2010)
[25] Podgurski, A., Clarke, L.A.: A formal model of program dependences and its implications for software testing, debugging, and maintenance. IEEE Trans. Softw. Eng. 16(9), 965-979 (1990)
[26] Ranganath, V.P., Amtoft, T., Banerjee, A., Dwyer, M.B., Hatcliff, J.: A new foundation for control-dependence and slicing for modern program structures. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 77-93. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31987-0_7 · Zbl 1108.68429
[27] Ranganath, V.P., Amtoft, T., Banerjee, A., Hatcliff, J., Dwyer, M.B.: A new foundation for control dependence and slicing for modern program structures. ACM Trans. Program. Lang. Syst. 29(5) (2007). http://doi.acm.org/10.1145/1275497.1275502 · Zbl 1108.68429
[28] Silva, J.: A vocabulary of program slicing-based techniques. ACM Comput. Surv. 44(3), 12:1-12:41 (2012) · Zbl 1293.68081
[29] Sivagurunathan, Y., Harman, M., Danicic, S.: Slicing, I/O and the implicit state. In: Proceedings of the Third International Workshop on Automatic Debugging: Linköping, Sweden, AADEBUG 1997, pp. 59-67. Linköping Electronic Articles in Computer and Information Science, May 1997
[30] Strobl, F., Wisspeintner, A.: Specification of an elevator control system - an autofocus case study. Technical report. TUM-I9906, Technische Universität München (1999)
[31] Tip, F.: A survey of program slicing techniques. J. Program. Lang. 3(3), 121-189 (1995)
[32] Wasserrab, D.: From formal semantics to verified slicing. Ph.D. thesis, Karlsruher Institut für Technologie (2010)
[33] Weiser, M.: Program slicing. IEEE Trans. Softw. Eng. 10(4), 352-357 (1984) · Zbl 0552.68004
[34] Weiser, M.D.: Program slices: formal, psychological, and practical investigations of an automatic program abstraction method. Ph.D. thesis, University of Michigan, Ann Arbor, MI (1979)
[35] Xu, B., Qian, J., Zhang, X., Wu, Z., Chen, L.: A brief survey of program slicing. ACM SIGSOFT Softw. Eng. Notes 30(2), 1-36 (2005)
[36] Zaghal, R.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.