Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

Net Meeting 26

Date estimated!

Review of Action List

The actions are all at Overture on SourceForge.

New items

Cool new Eclipse features discovered recently

News about the rCOS tool


Status and development plans for VDMTools version 8.xx
Nothing to report.


Overture Parser Update

Nothing to report.

Status of Adriana’s work on the Overture Test Automation Support

Adriana made the expanded version of the traces written by the user.

Status of Carlos’ work on the Overture Connector between VDM++ and JML

Carlos got the JML parser interacting with his mapper. He will continue mapping from VDM to JML in VDM++.

Status of Augusto’s work on the Overture Proof Obligation Generator

Augusto finished the implementation of the POG, apart from some minor things involving classes that are not working properly.

New students (Kenneth and Hans Christian)

Kenneth and Hans Christian will development a tool similar with Rose link from VDMTools. They will extend the overture project with an eclipse plugin (EMF) for going back and forth between VDM and UML. Additionally they will take a look at the test trace file and see if it is possible to pars this file into a UML sequence diagram.

The MONDEX case study

Jeremy and John have discussed a substantial paper on Mondex for FACJ with Jim Woodcock, who is planning a special issue on Mondex follow-up. The one thing John would like to show that was not done so far is a GUI for domain expert validation. John has a student who wants to work in this area but she is going to be part time and will take long. He is considering whether he can divert PhD? student resource on this at Newcastle.

The Pacemaker case study

Pacemaker FAQ is in the wiki at http://www.cas.mcmaster.ca/wiki/index.php/Pacemaker_FAQ The head of wiki is: http://www.cas.mcmaster.ca/wiki/index.php/Pacemaker John will give an invited talk on the pacemaker work as part of a GC day immediately preceding the ABZ conference in London in September. He will work further on Pacemaker before then.


Improvements were made in proving the proof obligations automatically in HOL. A vote of thanks to Hugo and Miguel is made for speaking at the GC workshop - it got the community a lot of good publicity and improved recognition in the GC community. They liked the way the community is using the challenges to explore and benchmark different aspects of the VDM technology. Miguel is preparing a page for the VDMPortal compiling all the material they have so far.

Publication plans

In preparation:

In review:

In press:

Recently Appeared:

Any other business

An Overture Summer School was suggested and it will be discussed in the next meeting. The members of the Overture community should take an action to investigate the rCOS plug-ins. A description of the rCos tool is available on http://rcos.iist.unu.edu/tool.

Next Meeting

20 July 2008, 1300 CET