ePubs

The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/35842
Record Status Checked
Record Id 35842
Title Mondex Case Study First Workshop
Contributors
Abstract The Mondex Case Study is being be used as an initial experiment for the Verified Software Repository. A number of research groups will work on the same problem in parallel. We have chosen as our problem the Mondex electronic purse work, which was originally specified and refined in Z, and proved correct by hand. That work was some ten years ago and we use this reworking to see what more can be done now compared to then. The kind of questions we hope to address are: What the current state of the art is in mechanising the specification, refinement, and proof? Can we get a full automation of this example? How can we combine the best of each approach? From the previous work we know that the case study will raise some challenging issues and so we hope that this new work to contribute to setting a research agenda for the repository. This Work is the slides and other material from the first workshop.
Organisation CCLRC , ESC , ASTeC-MaRS , VSR
Keywords Engineering , Verified Software Repository
Funding Information
Related Research Object(s):
Language English (EN)
Type Details URI(s) Local file(s) Year
Conference Proceedings First Workshop of Mondex Project of VSR-net. 2006 Mondex2.ref
Mondex1.mch
MONDEXworkshop1crocker.ppt
MONDEXworkshop1jones.ppt
AbWorld_proof.htm
AbWorld.pd
MONDEXworkshop1gogolla.pdf
AbWorld_proof.tex
MONDEXworkshop1stepney.ppt
MONDEXworkshopIntroduction.ppt
MONDEXworkshop1butler.ppt
MONDEXworkshop1king.pdf
2006
Showing record 1 of 1
RCUK
Science and Technology Facilities Council Switchboard: 01793 442000