Reification of Executable Test Scripts in Formal Specicifation-Based Test Generation: The Java Card Transaction Mechanism Case Study.