Formal specification and verification of JavaCard's application identifier class

DOI10.1007/3-540-45165-X_11MaRDI QIDQ2771757zbMATH OpenFDO

Authors Joachim van den Berg, Bart Jacobs, Erik Poll

Publication date 18 February 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2041/20410137

Mathematics Subject Classification ID

Theory of programming languages (68N15) Data encryption (aspects in computer science) (68P25) Computing methodologies and applications (68U99)

Review text

Summay:This paper discusses a verification in PVS of the \texttt{AID} (Application Identifier) class from the JavaCard API. The properties that are verified are formulated in the interface specification language JML. This language is also used to express the properties that are assumed about the native methods from the \texttt{Util} class that are used in the \texttt{AID} class. These properties include invariants for classes and behaviour specifications for methods; the latter give pre- and post-conditions describing the functional behaviour, and also specify when exceptions may be thrown. For the entire collection see [Zbl 0968.68557].

Recommendations

• scientific article; zbMATH DE number 1848384
• Algebraic Methodology and Software Technology
• A formal executable semantics of the JavaCard platform
• Fundamental Approaches to Software Engineering
• Formal methods for smart cards: an experience report

Cited in

(13)

• Coalgebras and monads in the semantics of Java
• Weakest pre-condition reasoning for Java programs with JML annotations
• Source code verification of a secure payment applet
• Formal specification and verification of JDK's identity hash map implementation
• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
• A dynamic logic for the formal verification of Java card programs
• JCML: A specification language for the runtime verification of Java card programs
• scientific article; zbMATH DE number 1848384 (Why is no real title available?)
• scientific article; zbMATH DE number 2090026 (Why is no real title available?)
• Specification and runtime verification of Java card programs
• Algebraic Methodology and Software Technology
• A case study in class library verification: Java's vector class
• Formal specification and verification of JDK's identity hash map implementation

Describes a project that uses

Uses Software

• JML

This page was built for publication: Formal specification and verification of JavaCard's application identifier class

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2771757)