Renaud De Landtsheer, Christophe Ponsard, Nicolas Devos. A Constraint-Solving Approach for Achieving Minimal-Reset Transition Coverage of Smartcard Behaviour, AVOCS’2014, Twente, Septembre 2014.
Smartcards are security critical devices requiring a high assurance verification approach. Although formal techniques can be used at design or even at development stages, such systems have to undergo a traditional hardware-in-the-loop testing phase. This phase is subject to two key requirements : firstly achieving exhaustive transition coverage of the behaviour of the system under test, and secondly minimising the testing time which is highly bound to a specific hardware reset operation. Model-based testing fits well given the availability of a precise model of the system behavior and its ability to produce high quality coverage, however it should also be able to cope with second performance requirement.
This paper presents an original algorithm addressing this problem by reformulating it as an integer programming problem to make a graph Eulerian. The associated cost criterion captures both the total length and number of resets in order to ensure a transition coverage. A MIP-based implementation of the algorithm was developed, benchmarked and integrated in an industrial smartcard testing framework. A validation case study from this domain is also presented. The approach can of course be applied to any other domains with similar near operation testing constraints.