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

03.05.2018 | Theme Section Paper

A method for testing and validating executable statechart models

verfasst von: Tom Mens, Alexandre Decan, Nikolaos I. Spanoudakis

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

Einloggen

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

search-config
loading …

Abstract

Statecharts constitute an executable language for modelling event-based reactive systems. The essential complexity of statechart models solicits the need for advanced model testing and validation techniques. In this article, we propose a method aimed at enhancing statechart design with a range of techniques that have proven their usefulness to increase the quality and reliability of source code. The method is accompanied by a process that flexibly accommodates testing and validation techniques such as test-driven development, behaviour-driven development, design by contract, and property statecharts that check for violations of behavioural properties during statechart execution. The method is supported by the Sismic tool, an open-source statechart interpreter library in Python, which supports all the aforementioned techniques. Based on this tooling, we carry out a controlled user study to evaluate the feasibility, usefulness and adequacy of the proposed techniques for statechart testing and validation.

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 Aravantinos, V., Voss, S., Teufl, S., Hölzl, F., Schätz, B.: AutoFOCUS 3: tooling concepts for seamless, model-based development of embedded systems. In: International Workshop on Model-Based Architecting of Cyber-Physical and Embedded Systems and International Workshop on UML Consistency Rules, Volume 1508 of CEUR Workshop Proceedings, pp. 19–26. CEUR-WS.org (2015) Aravantinos, V., Voss, S., Teufl, S., Hölzl, F., Schätz, B.: AutoFOCUS 3: tooling concepts for seamless, model-based development of embedded systems. In: International Workshop on Model-Based Architecting of Cyber-Physical and Embedded Systems and International Workshop on UML Consistency Rules, Volume 1508 of CEUR Workshop Proceedings, pp. 19–26. CEUR-WS.org (2015)
2.
Zurück zum Zitat Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
3.
Zurück zum Zitat Beck, K.: Test-Driven Development by Example. Addison-Wesley, Reading (2002) Beck, K.: Test-Driven Development by Example. Addison-Wesley, Reading (2002)
4.
Zurück zum Zitat Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: International Conference Computer Aided Verification (CAV), pp. 363–367. Springer (2001) Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: International Conference Computer Aided Verification (CAV), pp. 363–367. Springer (2001)
5.
Zurück zum Zitat Bunse, C., Klingert, S., Schulze, T.: Greenslas: supporting energy-efficiency through contracts. In: International Workshop on Energy Efficient Data Centers, pp. 54–68. Springer (2012) Bunse, C., Klingert, S., Schulze, T.: Greenslas: supporting energy-efficiency through contracts. In: International Workshop on Energy Efficient Data Centers, pp. 54–68. Springer (2012)
6.
Zurück zum Zitat Cabot, J., Clarisó, R., Riera, D.: On the verification of UML/OCL class diagrams using constraint programming. J. Syst. Softw. 93, 1–23 (2014)CrossRef Cabot, J., Clarisó, R., Riera, D.: On the verification of UML/OCL class diagrams using constraint programming. J. Syst. Softw. 93, 1–23 (2014)CrossRef
7.
Zurück zum Zitat Cariou, E., Ballagny, C., Feugas, A., Barbier, F.: Contracts for model execution verification. In: European Conference Modelling Foundations and Applications (ECMFA), Volume 6698 of Lecturer Notes in Computer Science, pp. 3–18. Springer (2011) Cariou, E., Ballagny, C., Feugas, A., Barbier, F.: Contracts for model execution verification. In: European Conference Modelling Foundations and Applications (ECMFA), Volume 6698 of Lecturer Notes in Computer Science, pp. 3–18. Springer (2011)
8.
Zurück zum Zitat Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333–348 (2015)CrossRef Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333–348 (2015)CrossRef
9.
Zurück zum Zitat Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby.: A language framework for expressing checkable properties of dynamic software. In: International SPIN Model Checking and Software Verification Workshop, Volume 1885 of Lecturer Notes in Computer Science, pp. 205–223. Springer (2000) Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby.: A language framework for expressing checkable properties of dynamic software. In: International SPIN Model Checking and Software Verification Workshop, Volume 1885 of Lecturer Notes in Computer Science, pp. 205–223. Springer (2000)
10.
Zurück zum Zitat Cossentino, M., Gaglio, S., Garro, A., Seidita, V.: Method fragments for agent design methodologies: from standardisation to research. Int. J. Agent Oriented Softw. Eng. 1(1), 91–121 (2007)CrossRef Cossentino, M., Gaglio, S., Garro, A., Seidita, V.: Method fragments for agent design methodologies: from standardisation to research. Int. J. Agent Oriented Softw. Eng. 1(1), 91–121 (2007)CrossRef
11.
Zurück zum Zitat Delmolino, K., Arnett, M., Kosba, A., Miller, A., Shi, E.: Step by step towards creating a safe smart contract: lessons and insights from a cryptocurrency lab. In: International Conference on Financial Cryptography and Data Security, pp. 79–94. Springer (2016) Delmolino, K., Arnett, M., Kosba, A., Miller, A., Shi, E.: Step by step towards creating a safe smart contract: lessons and insights from a cryptocurrency lab. In: International Conference on Financial Cryptography and Data Security, pp. 79–94. Springer (2016)
12.
Zurück zum Zitat Dietrich, I., Dressler, F., Dulz, W., German, R.: Validating UML simulation models with model-level unit tests. In: International Conference Simulation Tools and Techniques (SIMUTools) (2010) Dietrich, I., Dressler, F., Dulz, W., German, R.: Validating UML simulation models with model-level unit tests. In: International Conference Simulation Tools and Techniques (SIMUTools) (2010)
13.
Zurück zum Zitat Douglas, B.P.: Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns. Addison-Wesley, Reading (1999) Douglas, B.P.: Doing Hard Time: Developing Real-Time Systems with UML, Objects, Frameworks, and Patterns. Addison-Wesley, Reading (1999)
14.
Zurück zum Zitat Drusinsky, D.: Semantics and runtime monitoring of TLCharts: statechart automata with temporal logic conditioned transitions. In: Proceedings of the Fourth Workshop on Runtime Verification (RV 2004), Electronic Notes in Theoretical Computer Science, Volume 113, pp. 3–21 (2005) Drusinsky, D.: Semantics and runtime monitoring of TLCharts: statechart automata with temporal logic conditioned transitions. In: Proceedings of the Fourth Workshop on Runtime Verification (RV 2004), Electronic Notes in Theoretical Computer Science, Volume 113, pp. 3–21 (2005)
15.
Zurück zum Zitat Drusinsky, D.: Modeling and Verification Using UML Statecharts. Elsevier Science, Amsterdam (2006) Drusinsky, D.: Modeling and Verification Using UML Statecharts. Elsevier Science, Amsterdam (2006)
16.
Zurück zum Zitat Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: International Conference on Software Engineering, pp. 411–420. ACM (1999) Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: International Conference on Software Engineering, pp. 411–420. ACM (1999)
17.
Zurück zum Zitat Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1–3), 35–45 (2007)MathSciNetCrossRefMATH Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1–3), 35–45 (2007)MathSciNetCrossRefMATH
18.
Zurück zum Zitat Esmaeilsabzali, S., Day, N.A., Atlee, J.M., Niu, J.: Deconstructing the semantics of big-step modelling languages. Requir. Eng. 15(2), 235–265 (2010)CrossRef Esmaeilsabzali, S., Day, N.A., Atlee, J.M., Niu, J.: Deconstructing the semantics of big-step modelling languages. Requir. Eng. 15(2), 235–265 (2010)CrossRef
19.
Zurück zum Zitat Estler, H., Furia, C.A., Nordio, M., Piccioni, M., Meyer, B.: Contracts in practice. In: International Symposium on Formal Methods (FM), Volume 8442 of Lecturer Notes in Computer Science, pp. 230–246. Springer (2014) Estler, H., Furia, C.A., Nordio, M., Piccioni, M., Meyer, B.: Contracts in practice. In: International Symposium on Formal Methods (FM), Volume 8442 of Lecturer Notes in Computer Science, pp. 230–246. Springer (2014)
20.
Zurück zum Zitat Fabbri, S.C.P.F., Maldonado, J.C., Sugeta, T., Masiero, P.C.: Mutation testing applied to validate specifications based on statecharts. In: International Symposium on Software Reliability Engineering (ISSRE), pp. 210–219. IEEE Computer Society (1999) Fabbri, S.C.P.F., Maldonado, J.C., Sugeta, T., Masiero, P.C.: Mutation testing applied to validate specifications based on statecharts. In: International Symposium on Software Reliability Engineering (ISSRE), pp. 210–219. IEEE Computer Society (1999)
21.
Zurück zum Zitat Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. Eng. Dependable Softw. Syst. 34, 141–175 (2013) Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. Eng. Dependable Softw. Syst. 34, 141–175 (2013)
22.
Zurück zum Zitat Gnesi, S., Latella, D., Massink M.: Model checking UML statechart diagrams using JACK. In: International Symposium on High-Assurance Systems Engineering (HASE), pp. 46–55. IEEE Computer Society (1999) Gnesi, S., Latella, D., Massink M.: Model checking UML statechart diagrams using JACK. In: International Symposium on High-Assurance Systems Engineering (HASE), pp. 46–55. IEEE Computer Society (1999)
23.
Zurück zum Zitat Gogolla, M., Hamann, L., Hilken, F., Sedlmeier, M.: Modeling behavior with interaction diagrams in a UML and OCL tool. In: Behavior Modeling—Foundations and Applications, BM-FA 2009–2014, Revised Selected Papers, Volume 6368 of Lecturer Notes in Computer Science, pp. 31–58. Springer (2015) Gogolla, M., Hamann, L., Hilken, F., Sedlmeier, M.: Modeling behavior with interaction diagrams in a UML and OCL tool. In: Behavior Modeling—Foundations and Applications, BM-FA 2009–2014, Revised Selected Papers, Volume 6368 of Lecturer Notes in Computer Science, pp. 31–58. Springer (2015)
24.
Zurück zum Zitat Gogolla, M., Büttner, F., Richters, M.: USE: a UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69(1–3), 27–34 (2007)MathSciNetCrossRefMATH Gogolla, M., Büttner, F., Richters, M.: USE: a UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69(1–3), 27–34 (2007)MathSciNetCrossRefMATH
25.
Zurück zum Zitat Gomaa, H.: Designing Software Product Lines with UML: From Use Cases to Pattern-Based Software Architectures. Addison Wesley, Reading (2004) Gomaa, H.: Designing Software Product Lines with UML: From Use Cases to Pattern-Based Software Architectures. Addison Wesley, Reading (2004)
26.
Zurück zum Zitat Hamann, L., Hofrichter, O., Gogolla, M.: On integrating structure and behavior modeling with OCL. In: International Conference on Model Driven Engineering Languages and Systems, Volume 7590 of Lecturer Notes in Computer Science, pp. 235–251. Springer (2012) Hamann, L., Hofrichter, O., Gogolla, M.: On integrating structure and behavior modeling with OCL. In: International Conference on Model Driven Engineering Languages and Systems, Volume 7590 of Lecturer Notes in Computer Science, pp. 235–251. Springer (2012)
28.
Zurück zum Zitat Harel, D., Gery, E.: Executable object modeling with statecharts. IEEE Comput. 30(7), 31–42 (1997)CrossRef Harel, D., Gery, E.: Executable object modeling with statecharts. IEEE Comput. 30(7), 31–42 (1997)CrossRef
29.
Zurück zum Zitat Harel, D., Kugler, H.: The Rhapsody Semantics of Statecharts (or, on the Executable Core of the UML), Volume LNCS 3147. Springer, Berlin (2004) Harel, D., Kugler, H.: The Rhapsody Semantics of Statecharts (or, on the Executable Core of the UML), Volume LNCS 3147. Springer, Berlin (2004)
30.
Zurück zum Zitat Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), 293–333 (1996)CrossRef Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), 293–333 (1996)CrossRef
31.
Zurück zum Zitat Henderson-Sellers, B., Ralyté, J.: Situational method engineering: state-of-the-art review. J. Univers. Comput. Sci. 16(3), 424–478 (2010) Henderson-Sellers, B., Ralyté, J.: Situational method engineering: state-of-the-art review. J. Univers. Comput. Sci. 16(3), 424–478 (2010)
32.
Zurück zum Zitat Idelberger, F., Governatori, G., Riveret, R., Sartor, G.: Evaluation of logic-based smart contracts for blockchain systems. In: International Symposium on Rules and Rule Markup Languages for the Semantic Web, pp. 167–183. Springer (2016) Idelberger, F., Governatori, G., Riveret, R., Sartor, G.: Evaluation of logic-based smart contracts for blockchain systems. In: International Symposium on Rules and Rule Markup Languages for the Semantic Web, pp. 167–183. Springer (2016)
33.
Zurück zum Zitat Lazar, I., Motogna, S., Parv, B.: Behaviour-driven development of foundational UML components. Electron. Notes Theor. Comput. Sci. 264(1), 91–105 (2010). (Int’l Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA))CrossRef Lazar, I., Motogna, S., Parv, B.: Behaviour-driven development of foundational UML components. Electron. Notes Theor. Comput. Sci. 264(1), 91–105 (2010). (Int’l Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA))CrossRef
34.
Zurück zum Zitat Leavens, G.T., Cheon, Y.: Design by Contract with JML. Technical report, Iowa State University (2006) Leavens, G.T., Cheon, Y.: Design by Contract with JML. Technical report, Iowa State University (2006)
35.
Zurück zum Zitat Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebr. Program. 78(5), 293–303 (2009). (The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS’07))CrossRefMATH Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebr. Program. 78(5), 293–303 (2009). (The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS’07))CrossRefMATH
36.
Zurück zum Zitat Magee, J.: Behavioral analysis of software architectures using LTSA. In: International Conference on Software Engineering, pp. 634–637. ACM (1999) Magee, J.: Behavioral analysis of software architectures using LTSA. In: International Conference on Software Engineering, pp. 634–637. ACM (1999)
37.
Zurück zum Zitat Meyer, B.: Contract-driven development. In: International Conference on Fundamental Approaches to Software Engineering (FASE), Volume 4422 of Lecturer Notes in Computer Science, p. 11. Springer (2007) Meyer, B.: Contract-driven development. In: International Conference on Fundamental Approaches to Software Engineering (FASE), Volume 4422 of Lecturer Notes in Computer Science, p. 11. Springer (2007)
38.
Zurück zum Zitat Meyer, B.: Applying "design by contract". IEEE Comput. 25(10), 40–51 (1992)CrossRef Meyer, B.: Applying "design by contract". IEEE Comput. 25(10), 40–51 (1992)CrossRef
39.
Zurück zum Zitat North, D.: Behavior modification: the evolution of behavior-driven development. Better Software (2006) North, D.: Behavior modification: the evolution of behavior-driven development. Better Software (2006)
42.
Zurück zum Zitat OMG. Software and Systems Process Engineering Meta-Model Specification. Version 2.0. Technical Report OMG Document Number: Formal/2008-04-01. Object Management Group (2008) OMG. Software and Systems Process Engineering Meta-Model Specification. Version 2.0. Technical Report OMG Document Number: Formal/2008-04-01. Object Management Group (2008)
43.
Zurück zum Zitat Pei, Y., Furia, C.A., Nordio, M., Wei, Y., Meyer, B., Zeller, A.: Automated fixing of programs with contracts. IEEE Trans. Soft. Eng. 40(5), 427–449 (2014)CrossRef Pei, Y., Furia, C.A., Nordio, M., Wei, Y., Meyer, B., Zeller, A.: Automated fixing of programs with contracts. IEEE Trans. Soft. Eng. 40(5), 427–449 (2014)CrossRef
44.
Zurück zum Zitat Samek, M.: Practical UML Statecharts in C/C++: Event-Driven Programming for Embedded Systems, 2nd edn. CRC Press, Boca Raton (2008)CrossRef Samek, M.: Practical UML Statecharts in C/C++: Event-Driven Programming for Embedded Systems, 2nd edn. CRC Press, Boca Raton (2008)CrossRef
45.
Zurück zum Zitat Sen, K.: Concolic testing. In: International Conference on Automated Software Engineering, pp. 571–572. ACM (2007) Sen, K.: Concolic testing. In: International Conference on Automated Software Engineering, pp. 571–572. ACM (2007)
46.
Zurück zum Zitat Spanoudakis, N., Moraitis, P.: The agent modeling language (AMOLA). In: Dochev, D., Pistore, M., Traverso, P. (eds.) Artificial Intelligence: Methodology, Systems, and Applications, Volume 5253 of Lecture Notes in Computer Science, pp. 32–44. Springer, Berlin (2008) Spanoudakis, N., Moraitis, P.: The agent modeling language (AMOLA). In: Dochev, D., Pistore, M., Traverso, P. (eds.) Artificial Intelligence: Methodology, Systems, and Applications, Volume 5253 of Lecture Notes in Computer Science, pp. 32–44. Springer, Berlin (2008)
47.
Zurück zum Zitat Syriani, E., Vangheluwe, H., Mannadiar, R., Hansen, C., Van Mierlo, S., Ergin, H.: AToMPM: a web-based modeling environment. In: Joint Proceedings of MODELS’13 Invited Talks, Demonstration Session, Poster Session, and ACM Student Research Competition, Volume 1115, CEUR Workshop Proceedings (2013) Syriani, E., Vangheluwe, H., Mannadiar, R., Hansen, C., Van Mierlo, S., Ergin, H.: AToMPM: a web-based modeling environment. In: Joint Proceedings of MODELS’13 Invited Talks, Demonstration Session, Poster Session, and ACM Student Research Competition, Volume 1115, CEUR Workshop Proceedings (2013)
48.
Zurück zum Zitat Topalidou-Kyniazopoulou, A., Spanoudakis, N.I., Lagoudakis, M.G.: A CASE tool for robot behavior development. In: Chen, X., Stone, P., Sucar, L.E., Zant, T. (eds.) RoboCup 2012: Robot Soccer World Cup XVI. Lecture Notes in Computer Science, vol. 7500, pp. 225–236. Springer, Berlin (2013)CrossRef Topalidou-Kyniazopoulou, A., Spanoudakis, N.I., Lagoudakis, M.G.: A CASE tool for robot behavior development. In: Chen, X., Stone, P., Sucar, L.E., Zant, T. (eds.) RoboCup 2012: Robot Soccer World Cup XVI. Lecture Notes in Computer Science, vol. 7500, pp. 225–236. Springer, Berlin (2013)CrossRef
49.
Zurück zum Zitat Trakhtenbrot, M.: New mutations for evaluation of specification and implementation levels of adequacy in testing of statecharts models. In: Testing: Academic and Industrial Conference Practice and Research Techniques (MUTATION), pp. 151–160 (2007) Trakhtenbrot, M.: New mutations for evaluation of specification and implementation levels of adequacy in testing of statecharts models. In: Testing: Academic and Industrial Conference Practice and Research Techniques (MUTATION), pp. 151–160 (2007)
Metadaten
Titel
A method for testing and validating executable statechart models
verfasst von
Tom Mens
Alexandre Decan
Nikolaos I. Spanoudakis
Publikationsdatum
03.05.2018
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 2/2019
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-018-0676-3

Weitere Artikel der Ausgabe 2/2019

Software and Systems Modeling 2/2019 Zur Ausgabe