Rigorous Development of Java Card Applications

We present an approach to rigorous, tool supported design and development of Java Card applications. We employ the Unified Modelling Language (UML) and formal methods for object oriented software development in our approach. Our goal is to make Java Card applications robust "by design", to make the development process independent of the Java Card platform used and to enable applications to be verified by the KeY system. First we analyse the current situation of Java Card application development, then we present a real life Java Card case study and describe the problems we found that should be addressed by rigorous development. Finally we propose some solutions to selected problems by using UML specifications, software design patterns, formal specifications and a modern CASE tool support