Rigorous development of Java Card applications

Wojciech Mostowski

Abstract:

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.