Abstract
A transacted memory that is implemented using EEPROM technology offers persistence, undoability and auditing. The transacted memory system is formally specified in Z, and refined in two steps to a prototype C implementation / SPIN model. Conclusions are offered both on the transacted memory system itself and on the development process involving multiple notations and tools.
| Original language | English |
|---|---|
| Title of host publication | FME 2001: Formal Methods for Increasing Software Productivity |
| Subtitle of host publication | International Symposium of Formal Methods Europe Berlin, Germany, March 12–16, 2001, Proceedings |
| Editors | José Nuno Oliveira, Pamela Zave |
| Place of Publication | Berlin, Heidelberg |
| Publisher | Springer |
| Pages | 478-499 |
| Number of pages | 22 |
| ISBN (Electronic) | 978-3-540-45251-5 |
| ISBN (Print) | 978-3-540-41791-0 |
| DOIs | |
| Publication status | Published - Mar 2001 |
| Event | 10th International Symposium of Formal Methods Europe, FME 2001: Formal Methods for Increasing Software Productivity - Berlin, Germany Duration: 12 Mar 2001 → 16 Mar 2001 Conference number: 10 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 2021 |
Conference
| Conference | 10th International Symposium of Formal Methods Europe, FME 2001 |
|---|---|
| Abbreviated title | FME |
| Country/Territory | Germany |
| City | Berlin |
| Period | 12/03/01 → 16/03/01 |
Keywords
- SCS-Cybersecurity
- Information sequence
- Current generation
- Smart cards
- Spin model
- Memory manager
Fingerprint
Dive into the research topics of 'Transacted Memory for Smart Cards'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver