Mondex Case Study First Workshop

ePubs

The open archive for STFC research publications

Persistent URL	http://purl.org/net/epubs/work/35842
Record Status	Checked
Record Id	35842
Title	Mondex Case Study First Workshop
Contributors	JC Bicarregui (CCLRC Rutherford Appleton Lab.), JCP Woodcock (York U.), M Butler (Southampton U.), D Crocker (Escher Technologies), S King (York U.), CB Jones (Newcastle U.), M Gogolla (Bremen), S Stepney (York U.)
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):
Licence Information:
Language	English (EN)

Type	Details	URI(s)	Local file(s)	Year
Conference Proceedings	First Workshop of Mondex Project of VSR-net. 2006		MONDEXworkshopIntroduction.ppt MONDEXworkshop1stepney.ppt MONDEXworkshop1king.pdf MONDEXworkshop1butler.ppt Mondex1.mch Mondex2.ref MONDEXworkshop1jones.ppt MONDEXworkshop1crocker.ppt AbWorld.pd AbWorld_proof.htm AbWorld_proof.tex MONDEXworkshop1gogolla.pdf	2006