Model-Based MCDC Testing of Complex Decisions for the Java Card Applet Firewall
Roderick Bloem, Karin Greimel, Robert Könighofer, Franz Röck · 2013
Certification processes require the generation of models of a design. Using Model-Based Testing, these models can double as guides for test case generation. In this paper, we consider Boolean formulas that model a decision to be taken by a part of the software. We show how to use an SMT-solver to generate test cases that fulfill the MCDC coverage criteria on these models, in the presence of strong coupling. We show that the approach can improve test coverage, and finds a bug in an implementation of the Java Card Applet Firewall. Keywords—automatic test case generation; common criteria; java card applet firewall.