Case Studies

Below you can find the larger case studies that have been used in this project. They were used for development and testing purposes for both the translation and the proof system. The exact results on each of these cases can be found in http://www.overturetool.org/twiki/pub/Main/AutomaticProof/thesisSanderVermolen.pdf in the chapter 'Case Studies'.

Each of the cases below consists of three files:

1. ...vpp This is the most important file, it contains the sources of the case study. From this file, the following two can be generated.
2. ...vpp.app This is the abstract syntax tree of the source. It can be regenerated using the Overture parser and the file above as input.
3. ...POs.vpp This file contains a class with one static instance variable that is initialized to be a collection of all proof obligations for this specific case study. These proof obligations can be generated by using the VDMTools Integrity Checker, manually parsing the proof obligations and copying them into a collection (these manual steps are required since there is no Integrity checker available in the Overture project yet).

So the first of the above files is crucial, the other two are auxiliary. When just trying the translation, the last is not directly useful.

Alarm

1. alarm.vpp
2. alarm.vpp.app
3. alarmPOs.vpp

Memory

1. memory.vpp
2. memory.vpp.app
3. memoryPOs.vpp

Mondex-abstract

1. mondex-abstract.vpp
2. mondex-abstract.vpp.app
3. mondex-abstractPOs.vpp

Safer

1. safer.vpp
2. safer.vpp.app
3. saferPOs.vpp

Tracker

1. tracker.vpp
2. tracker.vpp.app
3. trackerPOs.vpp

-- SanderVermolen - 08 Sep 2007