Name
Abstract | ||
|---|---|---|
This paper presents a case study in the formal specification and verification of a smart card application. The application is an electronic purse implementation, developed by the smart card producer Gemplus as a test case for formal methods for smart cards. It has been annotated (by the authors) with specifications using the Java Modeling Language (JML), a language designed to specify the functional behavior of Java classes. The reason for using JML as a specification language is that several tools are available to check (parts of) the specification w.r.t, an implementation. These tools vary in their level of automation and in the level of correctness they ensure. Several of these tools have been used for the Gemplus case study. We discuss how the usage of these different tools is complementary: large parts of the specification can be checked automatically, while more precise verification methods can be used for the more intricate parts of the specification and implementation. We believe that having such a range of tools available for a single specification language is an important step towards the acceptance of formal methods in industry. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1016/j.scico.2004.05.011 | Sci. Comput. Program. |
Keywords | Field | DocType |
java modeling language,java card,formal verification,specification language,smartcard,smart cards,formal method,smart card | Specification language,Programming language,Programming language specification,Computer science,Correctness,Formal specification,Java Card,Formal methods,Java Modeling Language,Formal verification | Journal |
Volume | Issue | ISSN |
55 | 1-3 | 0167-6423 |
Citations | PageRank | References |
28 | 1.64 | 20 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Cees-Bart Breunesse | 1 | 41 | 3.71 |
| Nestor Cataño | 2 | 57 | 4.77 |
| Marieke Huisman | 3 | 28 | 1.64 |
| B. Jacobs | 4 | 1046 | 100.09 |