Skip to main content

2015 | OriginalPaper | Buchkapitel

Model-Based Robustness Testing in Event-B Using Mutation

verfasst von : Aymerick Savary, Marc Frappier, Michael Leuschel, Jean-Louis Lanet

Erschienen in: Software Engineering and Formal Methods

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

Robustness testing aims at finding errors in a system under invalid conditions, such as unexpected inputs. We propose a robustness testing approach for Event-B based on specification mutation and model-based testing. We assume that a specification describes the valid inputs of a system. By applying negation rules, we mutate the precondition of events to explore invalid behaviour. Tests are generated from the mutated specification using ProB. ProB has been adapted to efficiently process mutated events. Mutated events are statically checked for satisfiability and enability using constraint satisfaction, to prune the transition search space. This has dramatically improve the performance of test generation. The approach is applied to the Java Card bytecode verifier. Large mutated specifications (containing 921 mutated events) can be easily tackled to ensure a good coverage of the robustness test space.

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 "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!

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!

Literatur
1.
2.
Zurück zum Zitat Agrawal, et al.: Design of Mutant Operators for the C Programming Language. Technical report, Software Engineering Research Center, Purdue University (1989) Agrawal, et al.: Design of Mutant Operators for the C Programming Language. Technical report, Software Engineering Research Center, Purdue University (1989)
3.
Zurück zum Zitat Aichernig, B.K., Lorber, F.: Model-based Mutation Testing with Timed Automata. Technical report IST-MBT-2013-02, TU Graz, pp. 1–21 (2013) Aichernig, B.K., Lorber, F.: Model-based Mutation Testing with Timed Automata. Technical report IST-MBT-2013-02, TU Graz, pp. 1–21 (2013)
4.
Zurück zum Zitat Bouquet, F. et al.: A subset of precise UML for model-based testing. In: 3rd International Workshop on Advances in Model-based Testing, pp. 95–104. ACM (2007) Bouquet, F. et al.: A subset of precise UML for model-based testing. In: 3rd International Workshop on Advances in Model-based Testing, pp. 95–104. ACM (2007)
5.
Zurück zum Zitat Cavalcanti, A., Gaudel, M.-C.: Data flow coverage for circus-based testing. In: Gnesi, S., Rensink, A. (eds.) FASE 2014 (ETAPS). LNCS, vol. 8411, pp. 415–429. Springer, Heidelberg (2014) CrossRef Cavalcanti, A., Gaudel, M.-C.: Data flow coverage for circus-based testing. In: Gnesi, S., Rensink, A. (eds.) FASE 2014 (ETAPS). LNCS, vol. 8411, pp. 415–429. Springer, Heidelberg (2014) CrossRef
6.
Zurück zum Zitat Gargantini, A.: Using model checking to generate fault detecting tests. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 189–206. Springer, Heidelberg (2007) CrossRef Gargantini, A.: Using model checking to generate fault detecting tests. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 189–206. Springer, Heidelberg (2007) CrossRef
7.
Zurück zum Zitat Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649–678 (2011)CrossRef Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649–678 (2011)CrossRef
8.
Zurück zum Zitat Khurshid, S., Marinov, D.: TestEra: specification-based testing of java programs using SAT. Autom. Softw. Eng. 11(4), 403–434 (2004)CrossRef Khurshid, S., Marinov, D.: TestEra: specification-based testing of java programs using SAT. Autom. Softw. Eng. 11(4), 403–434 (2004)CrossRef
9.
Zurück zum Zitat Kim, S., Clark, J., McDermid, J.: The Rigorous Generation of Java Mutation Operators Using HAZOP. University of York, Technical report (1999) Kim, S., Clark, J., McDermid, J.: The Rigorous Generation of Java Mutation Operators Using HAZOP. University of York, Technical report (1999)
10.
Zurück zum Zitat Leuschel, M., Butler, M.: Prob: an automated analysis toolset for the b method. Int. J. Softw. Tools Technol. Transfer 10(2), 185–203 (2008)CrossRef Leuschel, M., Butler, M.: Prob: an automated analysis toolset for the b method. Int. J. Softw. Tools Technol. Transfer 10(2), 185–203 (2008)CrossRef
11.
Zurück zum Zitat Mikucionis, M., Larsen, K.G., Nielsen, B.: T-UPPAAL: Online model-based testing of real-time systems. In: 19\(^{th}\) Automated Software Engineering (ASE2004), pp. 396–397 (2004) Mikucionis, M., Larsen, K.G., Nielsen, B.: T-UPPAAL: Online model-based testing of real-time systems. In: 19\(^{th}\) Automated Software Engineering (ASE2004), pp. 396–397 (2004)
12.
Zurück zum Zitat Oracle Corporation: Java Card 3 Platform Virtual Machine Specification Oracle Corporation: Java Card 3 Platform Virtual Machine Specification
13.
14.
Zurück zum Zitat Satpathy, M., Butler, M., Leuschel, M., Ramesh, S.: Automatic testing from formal specifications. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 95–113. Springer, Heidelberg (2007) CrossRef Satpathy, M., Butler, M., Leuschel, M., Ramesh, S.: Automatic testing from formal specifications. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 95–113. Springer, Heidelberg (2007) CrossRef
15.
Zurück zum Zitat Savary, A., Frappier, M., Lanet, J.-L.: Detecting vulnerabilities in java-card bytecode verifiers using model-based testing. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 223–237. Springer, Heidelberg (2013) CrossRef Savary, A., Frappier, M., Lanet, J.-L.: Detecting vulnerabilities in java-card bytecode verifiers using model-based testing. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 223–237. Springer, Heidelberg (2013) CrossRef
16.
Zurück zum Zitat Shafique, M., Labiche, Y.: A systematic review of state-based test tools. Int. J. Softw. Tools Technol. Transfer 17(1), 59–76 (2015)CrossRef Shafique, M., Labiche, Y.: A systematic review of state-based test tools. Int. J. Softw. Tools Technol. Transfer 17(1), 59–76 (2015)CrossRef
17.
Zurück zum Zitat Utting, M., Legeard, B.: Practical Model Based Testing: A Tools Approach. Kaufmann, Morgan (2007) Utting, M., Legeard, B.: Practical Model Based Testing: A Tools Approach. Kaufmann, Morgan (2007)
18.
Zurück zum Zitat Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Software Testing Verification and Reliability 22(5), 297–312 (2012)CrossRef Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Software Testing Verification and Reliability 22(5), 297–312 (2012)CrossRef
Metadaten
Titel
Model-Based Robustness Testing in Event-B Using Mutation
verfasst von
Aymerick Savary
Marc Frappier
Michael Leuschel
Jean-Louis Lanet
Copyright-Jahr
2015
DOI
https://doi.org/10.1007/978-3-319-22969-0_10