From Finite State Machines to Provably Correct Java Card Applets

Abstract This paper presents a systematic approach to developing Java Card applets and/or formal specifications for them, starting from descriptions in the form of finite state machines. The formal specifications are written in the specification language JML, and can be checked against Java Card source code using the static checker ESC/Java.

• Type: Conference
• Year: 2003
• Where: SEC
• Authors: Engelbert Hubbers, Martijn Oostdijk, Erik Poll
• Keywords: Formal Specifications, Java Card, JAVA CARD Source, SEC 2003, SEC 2007