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 reallife 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.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences (hsv//eng)

Nyckelord

formal specification

Java

UML

Java Card

object-oriented design

OCL

Publikations- och innehållstyp

kon (ämneskategori)

vet (ämneskategori)