Generating Unit Tests from Formal Proofs

We present a new automatic test generation method for JAVA CARD based on attempts at formal verification of the implementation under test (IUT). Self-contained unit tests in JUnit format are generated automatically. The advantages of the approach are: (i) it exploits the full information available in the IUT and in its formal model giving very good hybrid coverage; (ii) a non-trivial formal model of the IUT is unnecessary; (iii) it is adaptable to the skills that users may possess in formal methods.

• Type: Conference
• Year: 2007
• Where: TAP
• Authors: Christian Engel, Reiner Hähnle
• Keywords: Formal Model, Formal Verification, Non-trivial Formal Model, TAP 2007