Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

Net Meeting 19

Date 8 July 2007, 1300 CET
Participants Peter Gorm Larsen, Hugo Macedo, Shin Sahara, Marcel Verhoef, Sander Vermolen

Review of Action List

The actions are all at Overture on SourceForge.


Status and development plans for VDMTools version 8.xx
Currently released 8.0 RC version including VICE, this version fixed many small bugs from IFAD era.
The VDM team got 2 new VDM users. The jobs still small, but we think this is the important step for VDM.
Bug reporting for VDMTools bugs
Fixed all bugs reported in English.
Seminar at the end of July in Japan
On 23rd and 24th July, VDM seminars will be hold in Tokyo and Nagoya. Peter, Marcel and Shin are speakers.


Status of Thomas’ work on the Overture type checker
Thesis now defended successfully with the Danish mark 10.
Status of Hugo’s work on the Overture interpreter
Studies on the requirements the interpreter need to fulfill in order to use Eclipse as an interface were done and on what’s the amount of effort to be done in the Eclipse side.
The conclusions so far are that it would be good to extend the specification of the interpreter and thus implementation to add functionality required by Eclipse GUI.
Status of Sander’s work on the Overture proof support
Sander is writing his thesis and have not developed anything anymore since he left Denmark. The estimate on how much it is possible to prove is above 60%, from that point on. In the writing pauses Sander will try to apply the tool to the RTRI and Pacemaker examples and report on the amount of proof that can be automated.
The MONDEX case study
Two mornings (15th and 22nd August) are planned to work on refinement between the Abstract and Concrete models. These will begin with a short tutorial on proof by John.
The Pacemaker case study
Marcel reported that Tom Maibaum is the professor from McMaster that has adopted the PACEMAKER case for the GC6 initiative and they are working (with Brian Larson) on setting up an initiative in north America for certifying this kind of applications. Basically, the Food and Drug Administration will make a standard to which all these kind of devices shall conform.
A workshop at FM’08 is planned as a side event for FM’08 aiming to assess how first responses to the pacemaker challenge would look like when trying to conform to this draft standard.
With the work done so far we are on the edge and we should try to be involved in the workshop planned to FM’08.
We decided to try Sander’s work to prove part of Hugo’s PACEMAKER.
New students from Minho for Overture
Currently the new students are planning to work on
  • Test automation
  • JML coupling

Publication plans

In preparation:

In review:

In press:

Recently Appeared:

Next Meeting

26 Aug 1300 CET