Skip to main content
main-content
Top

Hint

Swipe to navigate through the chapters of this book

2018 | OriginalPaper | Chapter

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

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

Published in: Computer Safety, Reliability, and Security

Publisher: Springer International Publishing

share
SHARE

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.
Footnotes
1
The challenge of distinguishing the corresponding desired and correct behavior from potentially incorrect behavior given a test case for a system under test.
 
Literature
1.
go back to reference 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.
go back to reference ISO26262: International Organization for standardization, road vehicles - functional safety (2009) ISO26262: International Organization for standardization, road vehicles - functional safety (2009)
3.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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)
Metadata
Title
Optimal Test Suite Generation for Modified Condition Decision Coverage Using SAT Solving
Authors
Takashi Kitamura
Quentin Maissonneuve
Eun-Hye Choi
Cyrille Artho
Angelo Gargantini
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-319-99130-6_9

Premium Partner