Journal article
Specification, proof, and model checking of the Mondex electronic purse using RAISE
In
Formal Aspects of Computing
—
2008, Volume 20, Issue 1, pp. 101-116
Abstract
This paper describes how the communication protocol of Mondex electronic purses can be specified and verified against desired security properties. The specification is developed by stepwise refinement using the RAISE formal specification language, RSL, and the proofs are made by translation to PVS and SAL.
The work is part of a year-long project contributing to the international grand challenge in verified software engineering.
| Language: | English |
|---|---|
| Publisher: | Springer-Verlag |
| Year: | 2008 |
| Pages: | 101-116 |
| Journal subtitle: | Applicable Formal Methods |
| ISSN: | 1433299x and 09345043 |
| Types: | Journal article |
| DOI: | 10.1007/s00165-007-0054-3 |
| ORCIDs: | Haxthausen, Anne Elisabeth |
Keywords
