Transacted Memory for Smart Cards

Transacted Memory offers persistence, undoability and auditing. We present a Java/JML Reference Model of the Transacted Memory system on the basis of our earlier separate Z model and C implementation. We conclude that Java/JML combines the advantages of a high level specification in the JML part (based on our Z model), with a detailed implementation in the Java part (based on our C implementation).

• Type: Conference
• Year: 2001
• Where: FM
• Authors: Pieter H. Hartel, Michael J. Butler, Eduard de Jong, Mark Longley
• Keywords: FM 2001, Formal Methods, Java/JML Reference Model, Memory Offers