Specification,proof, and model checking of the Mondex electronic purse using RAISE |
| |
| Authors: | Chris George Anne E. Haxthausen |
| |
| Affiliation: | (1) International Institute for Software Technology, United Nations University, Macao, UNU-IIST, PO Box 3058, Macao SAR, China;(2) Informatics and Mathematical Modelling, Technical University of Denmark, Lyngby, Denmark |
| |
| 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. J. C. P. Woodcock |
| |
| Keywords: | Formal methods RAISE PVS SAL Verification Mondex |
| 本文献已被 SpringerLink 等数据库收录！ |
|
