| Specification of the JavaCard API in JML Towards formal specification and verification of applets and API implementations (2008) | |||||||||||||||
Abstract | |||||||||||||||
| This paper reports on an effort to increase the reliability of JavaCard-based smart cards by means of formal specification and verification of JavaCard source code. As a first step, lightweight formal interface specifications, written in the specification language JML, have been developed for all the classes in the JavaCard API (version 2.1). They make many of the implicit assumptions underlying the current implementation explicit, and thus facilitate the use of this API and increase the reliability of the code that is based on it. Furthermore, the formal specifications are amenable to tool support, for verification purposes. 1 | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||