Rigorous Development of Java Card Applications
Wojciech Mostowski · 2002
We present an approach to rigorous, tool supported design and development of JavaCard applications. We employ the Unified Modelling Language (UML) and formal methods for object oriented software development in our approach. Our goal is to make JavaCard applications robust "by design", to make the development process independent of the JavaCard platform used and to enable applications to be verified by the KeY system. First we analyse the current situation of JavaCard application development, then we present a real life JavaCard 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.