Attacks against smart cards are getting ever more advanced and it is thus important to stay ahead on the security front.
Many different countermeasures exist to counter the attacks, but it can be difficult to choose appropriate countermeasures to protect a particular program.
The purpose of this report is to address this concern by analysing how bit flips, induced by fault attacks, can affect Java programs. Previous work defining formal semantics and fault models for a small Java Card inspired language, are extended to provide a tool for automatic conversion of Java bytecode to UPPAAL models. We use UPPAAL to verify security properties with respect to formalised fault models.