Skip to main content
Erschienen in: Software and Systems Modeling 2/2017

03.05.2015 | Regular Paper

Using contexts to extract models from code

verfasst von: Lucio Mauro Duarte, Jeff Kramer, Sebastian Uchitel

Erschienen in: Software and Systems Modeling | Ausgabe 2/2017

Einloggen

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

search-config
loading …

Abstract

Behaviour models facilitate the understanding and analysis of software systems by providing an abstract view of their behaviours and also by enabling the use of validation and verification techniques to detect errors. However, depending on the size and complexity of these systems, constructing models may not be a trivial task, even for experienced developers. Model extraction techniques can automatically obtain models from existing code, thus reducing the effort and expertise required of engineers and helping avoid errors often present in manually constructed models. Existing approaches for model extraction often fail to produce faithful models, either because they only consider static information, which may include infeasible behaviours, or because they are based only on dynamic information, thus relying on observed executions, which usually results in incomplete models. This paper describes a model extraction approach based on the concept of contexts, which are abstractions of concrete states of a program, combining static and dynamic information. Contexts merge some of the advantages of using either type of information and, by their combination, can overcome some of their problems. The approach is partially implemented by a tool called LTS Extractor, which translates information collected from execution traces produced by instrumented Java code to labelled transition systems (LTS), which can be analysed in an existing verification tool. Results from case studies are presented and discussed, showing that, considering a certain level of abstraction and a set of execution traces, the produced models are correct descriptions of the programs from which they were extracted. Thus, they can be used for a variety of analyses, such as program understanding, validation, verification, and evolution.

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!

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!

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!

Literatur
1.
Zurück zum Zitat Alur, R., Černý, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for java classes. In: ACM POPL, pp. 98–109. ACM, New York, NY, USA. doi:10.1145/1040305.1040314 Alur, R., Černý, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for java classes. In: ACM POPL, pp. 98–109. ACM, New York, NY, USA. doi:10.​1145/​1040305.​1040314
4.
Zurück zum Zitat Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: ACM POPL, pp. 1–3. ACM, New York, NY, USA (2002). doi:10.1145/565816.503274 Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: ACM POPL, pp. 1–3. ACM, New York, NY, USA (2002). doi:10.​1145/​565816.​503274
5.
Zurück zum Zitat Belinfante, A.: Jtorx: a tool for on-line model-driven test derivation and execution. In: Esparza, J., Majumdar, R. (eds.) TACAS, LNCS, vol. 6015, pp. 266–270. Springer, Berlin, Germany (2010) Belinfante, A.: Jtorx: a tool for on-line model-driven test derivation and execution. In: Esparza, J., Majumdar, R. (eds.) TACAS, LNCS, vol. 6015, pp. 266–270. Springer, Berlin, Germany (2010)
6.
Zurück zum Zitat Beschastnikh, I., Brun, Y., Ernst, M.D., Krishnamurthy, A.: Inferring models of concurrent systems from logs of their behavior with CSight. In: Jalote, P., Briand, L., van der Hoek, A. (eds.) ICSE, pp. 468–479. ACM, New York, NY, USA (2014). doi:10.1145/2568225.2568246 Beschastnikh, I., Brun, Y., Ernst, M.D., Krishnamurthy, A.: Inferring models of concurrent systems from logs of their behavior with CSight. In: Jalote, P., Briand, L., van der Hoek, A. (eds.) ICSE, pp. 468–479. ACM, New York, NY, USA (2014). doi:10.​1145/​2568225.​2568246
7.
Zurück zum Zitat Beschastnikh, I., Brun, Y., Schneider, S., Sloan, M., Ernst, M.D.: Leveraging existing instrumentation to automatically infer invariant-constrained models. In: ACM ESEC/FSE, pp. 267–277. ACM, Szeged, Hungary (2011). doi:10.1145/2025113.2025151 Beschastnikh, I., Brun, Y., Schneider, S., Sloan, M., Ernst, M.D.: Leveraging existing instrumentation to automatically infer invariant-constrained models. In: ACM ESEC/FSE, pp. 267–277. ACM, Szeged, Hungary (2011). doi:10.​1145/​2025113.​2025151
8.
Zurück zum Zitat Bodhuin, T., Pagnozzi, F., Santone, A.: Abstracting models from execution traces for performing formal verification. In: Šęzak, D., Kim, T-H., Kiumi, A., Jiang, T., Verner, J.,Abrahã, S. (eds.) ASEA 2009, CCIS, vol. 59, pp. 143–150. Springer, Berlin, Heidelberg (2009). doi:10.1007/978-3-642-10619-4_18 Bodhuin, T., Pagnozzi, F., Santone, A.: Abstracting models from execution traces for performing formal verification. In: Šęzak, D., Kim, T-H., Kiumi, A., Jiang, T., Verner, J.,Abrahã, S. (eds.) ASEA 2009, CCIS, vol. 59, pp. 143–150. Springer, Berlin, Heidelberg (2009). doi:10.​1007/​978-3-642-10619-4_​18
9.
Zurück zum Zitat Burtscher, M.: VPC3: a fast and effective trace-compression algorithm. ACM Perform. Eval. Rev. 32(1), 167–176 (2004)CrossRef Burtscher, M.: VPC3: a fast and effective trace-compression algorithm. ACM Perform. Eval. Rev. 32(1), 167–176 (2004)CrossRef
10.
Zurück zum Zitat Chaki, S., Clarke, E., Ouaknine, J., Sharygina, N., Sinha, N.: Concurrent software verification with states, events, and deadlocks. Form. Asp. Comput. 17(4), 461–483 (2005)CrossRefMATH Chaki, S., Clarke, E., Ouaknine, J., Sharygina, N., Sinha, N.: Concurrent software verification with states, events, and deadlocks. Form. Asp. Comput. 17(4), 461–483 (2005)CrossRefMATH
11.
Zurück zum Zitat Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE TSE 30(6), 388–402 (2004) Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE TSE 30(6), 388–402 (2004)
12.
Zurück zum Zitat Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. JACM 50(5), 752–794 (2003)MathSciNetCrossRefMATH Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. JACM 50(5), 752–794 (2003)MathSciNetCrossRefMATH
13.
Zurück zum Zitat Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge, Massachusetts, USA (1999) Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge, Massachusetts, USA (1999)
14.
Zurück zum Zitat Cook, J.E., Wolf, A.L.: Discovering models of software processes from event-based data. ACM ToSEM 7(3), 215–249 (1998)CrossRef Cook, J.E., Wolf, A.L.: Discovering models of software processes from event-based data. ACM ToSEM 7(3), 215–249 (1998)CrossRef
15.
Zurück zum Zitat Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Păsăreanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from java source code. In: ACM ICSE, pp. 439–448. IEEE, Limerick, Ireland (2000). doi:10.1145/337180.337234 Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Păsăreanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from java source code. In: ACM ICSE, pp. 439–448. IEEE, Limerick, Ireland (2000). doi:10.​1145/​337180.​337234
16.
Zurück zum Zitat Cordy, J.R., Dean, T.R., Malton, A.J., Schneider, K.A.: Source transformation in software engineering using the TXL transformation system. IST 44(13), 827–837 (2002) Cordy, J.R., Dean, T.R., Malton, A.J., Schneider, K.A.: Source transformation in software engineering using the TXL transformation system. IST 44(13), 827–837 (2002)
17.
Zurück zum Zitat Dallmeier, V., Knopp, N., Mallon, C., Hack, S., Zeller, A.: Generating test cases for specification mining. In: ACM ISSTA, pp. 85–96. ACM, Trento, Italy (2010). doi:10.1145/1831708.1831719 Dallmeier, V., Knopp, N., Mallon, C., Hack, S., Zeller, A.: Generating test cases for specification mining. In: ACM ISSTA, pp. 85–96. ACM, Trento, Italy (2010). doi:10.​1145/​1831708.​1831719
18.
Zurück zum Zitat Duarte, L., Kramer, J., Uchitel, S.: Towards faithful model extraction based on contexts. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE, LNCS, vol. 4961, pp. 101–115. Springer, Berlin, Germany (2008) Duarte, L., Kramer, J., Uchitel, S.: Towards faithful model extraction based on contexts. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE, LNCS, vol. 4961, pp. 101–115. Springer, Berlin, Germany (2008)
19.
Zurück zum Zitat Duarte, L.M.: Behaviour model extraction using context information. Ph.D. thesis, Imperial College London, University of London (2007) Duarte, L.M.: Behaviour model extraction using context information. Ph.D. thesis, Imperial College London, University of London (2007)
20.
Zurück zum Zitat Duarte, L.M., Kramer, J., Uchitel, S.: Model extraction using context information. In: Nierstrasz, O., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS, LNCS, vol. 4199, pp. 380–394. Springer, Berlin, Germany (2006) Duarte, L.M., Kramer, J., Uchitel, S.: Model extraction using context information. In: Nierstrasz, O., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS, LNCS, vol. 4199, pp. 380–394. Springer, Berlin, Germany (2006)
21.
Zurück zum Zitat Feng, L., Lundmark, S., Meinke, K., Niu, F., Sindhu, M., Wong, P.: Case studies in learning-based testing. In: Yenigün, H., Yilmaz, C., Ulrich, A. (eds.) Testing Software and Systems, LNCS, vol. 8254, pp. 164–179. Springer, Berlin, Heidelberg (2013) Feng, L., Lundmark, S., Meinke, K., Niu, F., Sindhu, M., Wong, P.: Case studies in learning-based testing. In: Yenigün, H., Yilmaz, C., Ulrich, A. (eds.) Testing Software and Systems, LNCS, vol. 8254, pp. 164–179. Springer, Berlin, Heidelberg (2013)
22.
Zurück zum Zitat Fernandez, J., Mounier, L., Pachon, C.: Property oriented test case generation. In: Petrenko, A., Ulrich, A. (eds.) FATES, LNCS, vol. 2931, pp. 147–163. Springer, Berlin, Heidelberg (2003) Fernandez, J., Mounier, L., Pachon, C.: Property oriented test case generation. In: Petrenko, A., Ulrich, A. (eds.) FATES, LNCS, vol. 2931, pp. 147–163. Springer, Berlin, Heidelberg (2003)
23.
Zurück zum Zitat Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: ACM PLDI, pp. 234–245. ACM, Berlin, Germany (2002). doi:10.1145/512529.512558 Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: ACM PLDI, pp. 234–245. ACM, Berlin, Germany (2002). doi:10.​1145/​512529.​512558
24.
25.
Zurück zum Zitat Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: ACM ESEC/FSE, pp. 257–266. ACM, Helsinki, Finland (2003). doi:10.1145/940071.940106 Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: ACM ESEC/FSE, pp. 257–266. ACM, Helsinki, Finland (2003). doi:10.​1145/​940071.​940106
26.
Zurück zum Zitat Giannakopoulou, D., Rakamarić, Z., Raman, V.: Symbolic learning of component interfaces. In: Proceedings of the 19th International Conference on Static Analysis, pp. 248–264 (2012) Giannakopoulou, D., Rakamarić, Z., Raman, V.: Symbolic learning of component interfaces. In: Proceedings of the 19th International Conference on Static Analysis, pp. 248–264 (2012)
27.
Zurück zum Zitat Gradara, S., Santone, A., Villani, M.L., Vaglini, G.: Model checking multithreaded programs by means of reduced models. ENTCS 110, 55–74 (2004) Gradara, S., Santone, A., Villani, M.L., Vaglini, G.: Model checking multithreaded programs by means of reduced models. ENTCS 110, 55–74 (2004)
28.
Zurück zum Zitat Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. LNCS 1254, 72–83 (1997) Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. LNCS 1254, 72–83 (1997)
29.
Zurück zum Zitat Havelund, K., Pressburger, T.: Model checking java programs using java pathFinder. STTT 2(4), 366–381 (2000)CrossRefMATH Havelund, K., Pressburger, T.: Model checking java programs using java pathFinder. STTT 2(4), 366–381 (2000)CrossRefMATH
30.
31.
Zurück zum Zitat Hoare, C.: Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, NJ, USA (1985) Hoare, C.: Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, NJ, USA (1985)
32.
Zurück zum Zitat Holzmann, G.: The model checker Spin. IEEE TSE 23(5), 279–295 (1997) Holzmann, G.: The model checker Spin. IEEE TSE 23(5), 279–295 (1997)
34.
Zurück zum Zitat Holzmann, G., Smith, M.: A practical method for verifying event-driven software. In: ACM ICSE, pp. 597–607. ACM, Los Angeles, USA (1999). doi:10.1145/302405.302710 Holzmann, G., Smith, M.: A practical method for verifying event-driven software. In: ACM ICSE, pp. 597–607. ACM, Los Angeles, USA (1999). doi:10.​1145/​302405.​302710
35.
Zurück zum Zitat Holzmann, G.J., Smith, M.: Software model checking: extracting verification models from source code. STVR 11(2), 65–79 (2001) Holzmann, G.J., Smith, M.: Software model checking: extracting verification models from source code. STVR 11(2), 65–79 (2001)
36.
Zurück zum Zitat Howar, F., Giannakopoulou, D., Rakamarić, Z.: Hybrid learning: interface generation through static, dynamic, and symbolic analysis. In: ACM ISSTA, pp. 268–279. ACM, Lugano, Switzerland (2013). doi:10.1145/2483760.2483783 Howar, F., Giannakopoulou, D., Rakamarić, Z.: Hybrid learning: interface generation through static, dynamic, and symbolic analysis. In: ACM ISSTA, pp. 268–279. ACM, Lugano, Switzerland (2013). doi:10.​1145/​2483760.​2483783
37.
Zurück zum Zitat Ichii, M., Myojin, T., Nakagawa, Y., Chikahisa, M., Ogawa, H.: A rule-based automated approach for extracting models from source code. In: Oliveto, R., Poshyvanyk, D., Cordy, J., Dean, T. (eds.) WCRE, pp. 308–317. IEEE, Kingston, ON, Canada (2012). doi:10.1109/WCRE.2012.40 Ichii, M., Myojin, T., Nakagawa, Y., Chikahisa, M., Ogawa, H.: A rule-based automated approach for extracting models from source code. In: Oliveto, R., Poshyvanyk, D., Cordy, J., Dean, T. (eds.) WCRE, pp. 308–317. IEEE, Kingston, ON, Canada (2012). doi:10.​1109/​WCRE.​2012.​40
40.
Zurück zum Zitat Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: P. Kemper (ed.) Proceedings of the Tools Session of Aachen 2001 International Multiconference on Measurement, Modelling and Evaluation of Computer-Communication Systems, pp. 7–12 (2001) Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: P. Kemper (ed.) Proceedings of the Tools Session of Aachen 2001 International Multiconference on Measurement, Modelling and Evaluation of Computer-Communication Systems, pp. 7–12 (2001)
41.
Zurück zum Zitat Leuschel, M., Massart, T., Currie, A.: How to make FDR Spin: LTL model checking of CSP by refinement. LNCS 2021, 99–118 (2001)MATH Leuschel, M., Massart, T., Currie, A.: How to make FDR Spin: LTL model checking of CSP by refinement. LNCS 2021, 99–118 (2001)MATH
42.
Zurück zum Zitat Li, H.F., Rilling, J., Goswami, D.: Granularity-driven dynamic predicate slicing algorithms for message passing systems. ASE 11(1), 63–89 (2004) Li, H.F., Rilling, J., Goswami, D.: Granularity-driven dynamic predicate slicing algorithms for message passing systems. ASE 11(1), 63–89 (2004)
43.
Zurück zum Zitat Lorenzoli, D., Mariani, L., Pezzè, M.: Automatic generation of software behavioral models. In: ACM ICSE, pp. 501–510. ACM, Leipzig, Germany (2008). doi:10.1145/1368088.1368157 Lorenzoli, D., Mariani, L., Pezzè, M.: Automatic generation of software behavioral models. In: ACM ICSE, pp. 501–510. ACM, Leipzig, Germany (2008). doi:10.​1145/​1368088.​1368157
44.
Zurück zum Zitat Machado, P.D.L., Silva, D., Mota, A.C.: Towards property oriented testing. ENTCS 184, 3–19 (2007)MATH Machado, P.D.L., Silva, D., Mota, A.C.: Towards property oriented testing. ENTCS 184, 3–19 (2007)MATH
45.
Zurück zum Zitat Magee, J., Kramer, J.: Concurrency: State Models and Java Programming, 2nd edn. Wiley, Chichester, England (2006)MATH Magee, J., Kramer, J.: Concurrency: State Models and Java Programming, 2nd edn. Wiley, Chichester, England (2006)MATH
46.
Zurück zum Zitat Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York, USA (1992)CrossRefMATH Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York, USA (1992)CrossRefMATH
47.
Zurück zum Zitat Mariani, L.: Behavior capture and test: dynamic analysis of component-based systems. Ph.d., Università degli Studi di Milano Bicocca (2005) Mariani, L.: Behavior capture and test: dynamic analysis of component-based systems. Ph.d., Università degli Studi di Milano Bicocca (2005)
48.
Zurück zum Zitat Meinke, K., Niu, F., Sindhu, M.: Learning-based software testing: a tutorial. In: Hähnle, R., Knoop, J., Margaria, T., Schreiner, D., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification, and Validation, Communications in Computer and Information Science, pp. 200–219. Springer, Berlin, Germany (2012) Meinke, K., Niu, F., Sindhu, M.: Learning-based software testing: a tutorial. In: Hähnle, R., Knoop, J., Margaria, T., Schreiner, D., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification, and Validation, Communications in Computer and Information Science, pp. 200–219. Springer, Berlin, Germany (2012)
49.
Zurück zum Zitat Meinke, K., Sindhu, M.: Incremental learning-based testing for reactive systems. In: Gogolla, M., Wolff, B. (eds.) Tests and Proofs, LNCS, vol. 6706, pp. 134–151. Springer, Berlin, Germany (2011)CrossRef Meinke, K., Sindhu, M.: Incremental learning-based testing for reactive systems. In: Gogolla, M., Wolff, B. (eds.) Tests and Proofs, LNCS, vol. 6706, pp. 134–151. Springer, Berlin, Germany (2011)CrossRef
50.
Zurück zum Zitat Milner, R.: An algebraic definition of simulation between programs. In: Society, B.C. (ed.) 2nd IJCAI, pp. 481–489. Morgan Kaufmann Publishers Inc., London, England (1971) Milner, R.: An algebraic definition of simulation between programs. In: Society, B.C. (ed.) 2nd IJCAI, pp. 481–489. Morgan Kaufmann Publishers Inc., London, England (1971)
51.
Zurück zum Zitat Milner, R.: Communication and Concurrency. Prentice-Hall Inc, Passau, Germany (1989)MATH Milner, R.: Communication and Concurrency. Prentice-Hall Inc, Passau, Germany (1989)MATH
53.
Zurück zum Zitat Odom, J., Hollingsworth, J., DeRose, L., Ekanadham, K., Sbaraglia, S.: Using dynamic tracing sampling to measure long running programs. In: ACM/IEEE SC, p. 59. IEEE, Seattle, WA, USA (2005). doi:10.1109/SC.2005.77 Odom, J., Hollingsworth, J., DeRose, L., Ekanadham, K., Sbaraglia, S.: Using dynamic tracing sampling to measure long running programs. In: ACM/IEEE SC, p. 59. IEEE, Seattle, WA, USA (2005). doi:10.​1109/​SC.​2005.​77
54.
Zurück zum Zitat Pradel, M., Gross, T.R.: Automatic generation of object usage specifications from large method traces. In: Ceballos, S. (ed.) IEEE/ACM ASE, pp. 371–382. IEEE Computer Society, Washington, DC, USA (2009). doi:10.1109/ASE.2009.60 Pradel, M., Gross, T.R.: Automatic generation of object usage specifications from large method traces. In: Ceballos, S. (ed.) IEEE/ACM ASE, pp. 371–382. IEEE Computer Society, Washington, DC, USA (2009). doi:10.​1109/​ASE.​2009.​60
55.
Zurück zum Zitat Raffelt, H., Steffen, B., Berg, T., Margaria, T.: LearnLib: a framework for extrapolating behavioral models. STTT 11(5), 393–407 (2009)CrossRef Raffelt, H., Steffen, B., Berg, T., Margaria, T.: LearnLib: a framework for extrapolating behavioral models. STTT 11(5), 393–407 (2009)CrossRef
56.
Zurück zum Zitat Strom, R.E., Yemini, S.: Typestate: a programming language concept for enhancing software reliability. IEEE TSE 12(1), 157–171 (1986)MATH Strom, R.E., Yemini, S.: Typestate: a programming language concept for enhancing software reliability. IEEE TSE 12(1), 157–171 (1986)MATH
57.
Zurück zum Zitat Utting, M.: How to Design Extended Finite State Machine Test Models in Java. CRC Press, Boca Raton, FL, USA (2011) Utting, M.: How to Design Extended Finite State Machine Test Models in Java. CRC Press, Boca Raton, FL, USA (2011)
58.
Zurück zum Zitat Utting, M., Legeard, B.: Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann Publishers Inc, San Francisco, CA, USA (2007) Utting, M., Legeard, B.: Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann Publishers Inc, San Francisco, CA, USA (2007)
59.
Zurück zum Zitat Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. ASE 10(2), 203–232 (2003) Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. ASE 10(2), 203–232 (2003)
60.
Zurück zum Zitat Walkinshaw, N., Bogdanov, K., Holcombe, M., Salahuddin, S.: Reverse engineering state machines by interactive grammar inference. In: Penta, M.D., Maletic, J.I. (eds.) WCRE, pp. 209–218. IEEE Computer Society, Washington, DC, USA (2007). doi:10.1109/WCRE.2007.45 Walkinshaw, N., Bogdanov, K., Holcombe, M., Salahuddin, S.: Reverse engineering state machines by interactive grammar inference. In: Penta, M.D., Maletic, J.I. (eds.) WCRE, pp. 209–218. IEEE Computer Society, Washington, DC, USA (2007). doi:10.​1109/​WCRE.​2007.​45
61.
Zurück zum Zitat Walkinshaw, N., Taylor, R., Derrick, J.: Inferring extended finite state machine models from software executions. In: Lähmmel, R., Oliveto, R., Robbes, R. (eds.) WCRE, pp.301–310. IEEE, Koblenz, Germany (2013). doi:10.1109/WCRE.2013.6671305 Walkinshaw, N., Taylor, R., Derrick, J.: Inferring extended finite state machine models from software executions. In: Lähmmel, R., Oliveto, R., Robbes, R. (eds.) WCRE, pp.301–310. IEEE, Koblenz, Germany (2013). doi:10.​1109/​WCRE.​2013.​6671305
62.
63.
Zurück zum Zitat Yu, Y., Wang, Y., Mylopoulos, J., Liaskos, S., Lapouchnian, A., Sampaio do Prado Leite, J.: Reverse engineering goal models from legacy code. In: IEEE RE, pp. 363–372. IEEE, Paris, France (2005). doi:10.1109/RE.2005.61 Yu, Y., Wang, Y., Mylopoulos, J., Liaskos, S., Lapouchnian, A., Sampaio do Prado Leite, J.: Reverse engineering goal models from legacy code. In: IEEE RE, pp. 363–372. IEEE, Paris, France (2005). doi:10.​1109/​RE.​2005.​61
Metadaten
Titel
Using contexts to extract models from code
verfasst von
Lucio Mauro Duarte
Jeff Kramer
Sebastian Uchitel
Publikationsdatum
03.05.2015
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 2/2017
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-015-0466-0

Weitere Artikel der Ausgabe 2/2017

Software and Systems Modeling 2/2017 Zur Ausgabe

Premium Partner