Voltar
Artigo Acesso aberto Revisado por pares
BIBTEX RIS

Formal specification of the JavaCard API in JML: the APDU class

2001; Elsevier BV; Volume: 36; Issue: 4 Linguagem: Inglês

10.1016/s1389-1286(01)00163-3

ISSN

1872-7069

Autores

Erik Poll, Joachim van den Berg, Bart Jacobs,

Tópico(s)

Formal Methods in Verification

Resumo

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, formal interface specifications, written in the specification language JML (Java Modeling Language), have been developed for all the classes that make up the JavaCard API. These specifications are "lightweight" in the sense that they are incomplete and specify only some aspects of the API, but they already provide a useful addition to the existing informal API specifications. Moreover, the fact that these specification are written in a formal language makes them amenable to tool support, for verification purposes. As an illustration, the JML specifications of the APDU (Application Protocol Data Unit) class in the JavaCard API are discussed in detail.

Referência(s)