nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Correctly Slicing Extended Finite State Machines

verfasst von : Torben Amtoft, Kelly Androutsopoulos, David Clark

Erschienen in: From Lambda Calculus to Cybersecurity Through Program Analysis

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

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 Danicic et alia. 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).

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Incremental Abstract Interpretation

Nächstes Kapitel Secure Guarded Commands

Nur mit Berechtigung zugänglich

Published as Research Note RN/13/22 from University College London.

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.002MathSciNetCrossRefMATH

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)CrossRef

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)CrossRef

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_15CrossRef

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)

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/BFb0019410CrossRef

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

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_6CrossRef

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)MathSciNetCrossRef

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.2160929CrossRef

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_13CrossRef

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)CrossRef

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_1CrossRef

17.

Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. High.-Order Symb. Comput. 13(4), 315–353 (2000)CrossRef

18.

Ilie, L., Yu, S.: Reducing NFAs by invariant equivalences. Theoret. Comput. Sci. 306(1–3), 373–390 (2003)MathSciNetCrossRef

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-3CrossRefMATH

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_12CrossRef

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_1CrossRef

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)CrossRef

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_7CrossRefMATH

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

28.

Silva, J.: A vocabulary of program slicing-based techniques. ACM Comput. Surv. 44(3), 12:1–12:41 (2012)CrossRef

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)CrossRef

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)CrossRef

36.

Zaghal, R.Y., Khan, J.I.: EFSM/SDL modeling of the original TCP standard (RFC793) and the congestion control mechanism of TCP Reno. Technical report. TR2005-07-22, Networking and Media Communications Research Laboratories, Department of Computer Science, Kent State University, July 2005 (2005)

Titel: Correctly Slicing Extended Finite State Machines
verfasst von: Torben Amtoft
Kelly Androutsopoulos
David Clark
Verlag: Springer International Publishing
Buch: From Lambda Calculus to Cybersecurity Through Program Analysis
Print ISBN: 978-3-030-41102-2

Electronic ISBN: 978-3-030-41103-9

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-41103-9_6

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner