Skip to main content
main-content

Tipp

Weitere Kapitel dieses Buchs durch Wischen aufrufen

2018 | OriginalPaper | Buchkapitel

Optimal Test Suite Generation for Modified Condition Decision Coverage Using SAT Solving

verfasst von: Takashi Kitamura, Quentin Maissonneuve, Eun-Hye Choi, Cyrille Artho, Angelo Gargantini

Erschienen in: Computer Safety, Reliability, and Security

Verlag: Springer International Publishing

share
TEILEN

Abstract

Boolean expressions occur frequently in descriptions of computer systems, but they tend to be complex and error-prone in complex systems. The modified condition decision coverage (MCDC) criterion in system testing is an important testing technique for Boolean expression, as its usage mandated by safety standards such as DO-178 [1] (avionics) and ISO26262 [2] (automotive). In this paper, we develop an algorithm to generate optimal MCDC test suites for Boolean expressions. Our algorithm is based on SAT solving and generates minimal MCDC test suites. Experiments on a real-world avionics system confirm that the technique can construct minimal MCDC test suites within reasonable times, and improves significantly upon prior techniques.
Fußnoten
1
The challenge of distinguishing the corresponding desired and correct behavior from potentially incorrect behavior given a test case for a system under test.
 
Literatur
1.
Zurück zum Zitat RTCA: DO-178C: Software considerations in airborne systems and equipment certification (2011) RTCA: DO-178C: Software considerations in airborne systems and equipment certification (2011)
2.
Zurück zum Zitat ISO26262: International Organization for standardization, road vehicles - functional safety (2009) ISO26262: International Organization for standardization, road vehicles - functional safety (2009)
3.
Zurück zum Zitat Chilenski, J.J., Miller, S.P.: Applicability of modified condition/decision coverage to software testing. Softw. Eng. J. 9(5), 193–200 (1994) CrossRef Chilenski, J.J., Miller, S.P.: Applicability of modified condition/decision coverage to software testing. Softw. Eng. J. 9(5), 193–200 (1994) CrossRef
4.
Zurück zum Zitat Ammann, P., Offutt, J.: Introduction to Software Testing. Cambridge University Press, Cambridge (2008) CrossRef Ammann, P., Offutt, J.: Introduction to Software Testing. Cambridge University Press, Cambridge (2008) CrossRef
5.
Zurück zum Zitat Kelly J.H., Dan S.V., John J.C., Leanna K.R.: A practical tutorial on modified condition/decision coverage. Technical report NASA/TM-2001-210876, NASA (2001) Kelly J.H., Dan S.V., John J.C., Leanna K.R.: A practical tutorial on modified condition/decision coverage. Technical report NASA/TM-2001-210876, NASA (2001)
8.
Zurück zum Zitat Weyuker, E.J., Goradia, T., Singh, A.: Automatically generating test data from a boolean specification. IEEE Trans. Softw. Eng. 20(5), 353–363 (1994) CrossRef Weyuker, E.J., Goradia, T., Singh, A.: Automatically generating test data from a boolean specification. IEEE Trans. Softw. Eng. 20(5), 353–363 (1994) CrossRef
9.
Zurück zum Zitat Dupuy, A., Leveson, N.: An empirical evaluation of the MC/DC coverage criterion on the HETE-2 satellite software. In: Proceedings of the 19th Digital Avionics Systems Conference (DASC 2000) (2000) Dupuy, A., Leveson, N.: An empirical evaluation of the MC/DC coverage criterion on the HETE-2 satellite software. In: Proceedings of the 19th Digital Avionics Systems Conference (DASC 2000) (2000)
10.
Zurück zum Zitat Vilkomir, S., Starov, O., Bhambroo, R.: Evaluation of T-wise approach for testing logical expressions in software. In: Proceedings of the Sixth IEEE International Conference on Software Testing, Verification and Validation, ICST 2013 Workshops Luxembourg, pp. 249–256 (2013) Vilkomir, S., Starov, O., Bhambroo, R.: Evaluation of T-wise approach for testing logical expressions in software. In: Proceedings of the Sixth IEEE International Conference on Software Testing, Verification and Validation, ICST 2013 Workshops Luxembourg, pp. 249–256 (2013)
11.
Zurück zum Zitat Kapoor, K., Bowen, J.P.: A formal analysis of MCDC and RCDC test criteria. Softw. Test., Verif. Reliab. 15(1) 21–40 (2005) Kapoor, K., Bowen, J.P.: A formal analysis of MCDC and RCDC test criteria. Softw. Test., Verif. Reliab. 15(1) 21–40 (2005)
13.
Zurück zum Zitat Jones, J.A., Harrold, M.J.: Test-suite reduction and prioritization for modified condition/decision coverage. IEEE Trans. Softw. Eng. 29(3), 195–209 (2003) CrossRef Jones, J.A., Harrold, M.J.: Test-suite reduction and prioritization for modified condition/decision coverage. IEEE Trans. Softw. Eng. 29(3), 195–209 (2003) CrossRef
14.
Zurück zum Zitat Arcaini, P., Gargantini, A., Riccobene, E.: How to optimize the use of SAT and SMT solvers for test generation of boolean expressions. Comput. J. 58(11), 2900–2920 (2015) CrossRef Arcaini, P., Gargantini, A., Riccobene, E.: How to optimize the use of SAT and SMT solvers for test generation of boolean expressions. Comput. J. 58(11), 2900–2920 (2015) CrossRef
15.
Zurück zum Zitat Chilenski, J.J.: An investigation of three forms of the modified condition decision coverage (MCDC) criterion. Technical report DOT/FAA/AR-01/18, Office of Aviation Research (2001) Chilenski, J.J.: An investigation of three forms of the modified condition decision coverage (MCDC) criterion. Technical report DOT/FAA/AR-01/18, Office of Aviation Research (2001)
16.
Zurück zum Zitat Vilkomir, S.A., Bowen, J.P.: From MC/DC to RC/DC: formalization and analysis of control-flow testing criteria. In: Formal Methods and Testing, an Outcome of the FORTEST Network, Revised Selected Papers, pp. 240–270 (2008) Vilkomir, S.A., Bowen, J.P.: From MC/DC to RC/DC: formalization and analysis of control-flow testing criteria. In: Formal Methods and Testing, an Outcome of the FORTEST Network, Revised Selected Papers, pp. 240–270 (2008)
17.
Zurück zum Zitat Whalen, M.W., Gay, G., You, D., Heimdahl, M.P.E., Staats, M.: Observable modified condition/decision coverage. In: 35th International Conference on Software Engineering ICSE 2013, San Francisco, CA, USA, pp. 102–111 (2013) Whalen, M.W., Gay, G., You, D., Heimdahl, M.P.E., Staats, M.: Observable modified condition/decision coverage. In: 35th International Conference on Software Engineering ICSE 2013, San Francisco, CA, USA, pp. 102–111 (2013)
18.
Zurück zum Zitat Offutt, A.J., Liu, S., Abdurazik, A., Ammann, P.: Generating test data from state-based specifications. Softw. Test., Verif. Reliab. 13(1) pp. 25–53 (2003) Offutt, A.J., Liu, S., Abdurazik, A., Ammann, P.: Generating test data from state-based specifications. Softw. Test., Verif. Reliab. 13(1) pp. 25–53 (2003)
19.
Zurück zum Zitat Bloem, R., Greimel, K., Koenighofer, R., Roeck, F.: Model-based MCDC testing of complex decisions for the Java Card Applet Firewall. In: Proceedings of the Fifth International Conference on Advances in System Testing and Validation Lifecycle (VALID 2013), pp. 1–6 (2013) Bloem, R., Greimel, K., Koenighofer, R., Roeck, F.: Model-based MCDC testing of complex decisions for the Java Card Applet Firewall. In: Proceedings of the Fifth International Conference on Advances in System Testing and Validation Lifecycle (VALID 2013), pp. 1–6 (2013)
21.
Zurück zum Zitat Yamada, A., Kitamura, T., Artho, C., Choi, E.H., Oiwa, Y., Biere, A.: Optimization of combinatorial testing by incremental SAT solving. In: Proceedings of the 8th IEEE International Conference on Software Testing, Verification and Validation (ICST 2015), pp. 1–10 (2015) Yamada, A., Kitamura, T., Artho, C., Choi, E.H., Oiwa, Y., Biere, A.: Optimization of combinatorial testing by incremental SAT solving. In: Proceedings of the 8th IEEE International Conference on Software Testing, Verification and Validation (ICST 2015), pp. 1–10 (2015)
23.
Zurück zum Zitat Heimdahl, M.P.E., Devaraj, G.: On the effect of test-suite reduction on automatically generated model-based tests. Autom. Softw. Eng. 14(1), 37–57 (2007) CrossRef Heimdahl, M.P.E., Devaraj, G.: On the effect of test-suite reduction on automatically generated model-based tests. Autom. Softw. Eng. 14(1), 37–57 (2007) CrossRef
24.
Zurück zum Zitat Gargantini, A., Heitmeyer, C.L.: Using model checking to generate tests from requirements specifications. In: Proceedings of the 7th European Conference of Software Engineering, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 1999), pp. 146–162 (1999) Gargantini, A., Heitmeyer, C.L.: Using model checking to generate tests from requirements specifications. In: Proceedings of the 7th European Conference of Software Engineering, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 1999), pp. 146–162 (1999)
25.
Zurück zum Zitat Pandita, R., Xie, T., Tillmann, N., de Halleux, J.: Guided test generation for coverage criteria. In: Proceedings of the 26th IEEE International Conference on Software Maintenance (ICSM 2010), Timisoara, Romania, pp. 1–10 (2010) Pandita, R., Xie, T., Tillmann, N., de Halleux, J.: Guided test generation for coverage criteria. In: Proceedings of the 26th IEEE International Conference on Software Maintenance (ICSM 2010), Timisoara, Romania, pp. 1–10 (2010)
26.
Zurück zum Zitat Bokil, P., Darke, P., Shrotri, U., Venkatesh, R.: Automatic test data generation for C programs. In: Proceedings of the Third IEEE International Conference on Secure Software Integration and Reliability Improvement SSIRI 2009, pp. 359–368 (2009) Bokil, P., Darke, P., Shrotri, U., Venkatesh, R.: Automatic test data generation for C programs. In: Proceedings of the Third IEEE International Conference on Secure Software Integration and Reliability Improvement SSIRI 2009, pp. 359–368 (2009)
27.
Zurück zum Zitat Awedikian, Z., Ayari, K., Antoniol, G.: MC/DC automatic test input data generation. In: Proceedings of the Genetic and Evolutionary Computation Conference (GECCO 2009), Canada, pp. 1657–1664 (2009) Awedikian, Z., Ayari, K., Antoniol, G.: MC/DC automatic test input data generation. In: Proceedings of the Genetic and Evolutionary Computation Conference (GECCO 2009), Canada, pp. 1657–1664 (2009)
Metadaten
Titel
Optimal Test Suite Generation for Modified Condition Decision Coverage Using SAT Solving
verfasst von
Takashi Kitamura
Quentin Maissonneuve
Eun-Hye Choi
Cyrille Artho
Angelo Gargantini
Copyright-Jahr
2018
DOI
https://doi.org/10.1007/978-3-319-99130-6_9

Premium Partner