Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

Net Meeting 20

Date 26 August 2007, 1300 CET
Participants John Fitzgerald,Peter Gorm Larsen, Hugo Macedo, Shin Sahara, Emma Nicholls

Review of Action List

The actions are all at Overture on SourceForge.


Status and development plans for VDMTools version 8.xx
Shin reported the development plan in this year is:
  • make VDM++TesK like test case generator prototype


:*make BIT, BYTE class as standard library

Functionality required by an important customer.

Actually trying to get the third user from the embedded system world, the important point is how to write a requirement specification for embedded systems. And, important point in the near future is how to connect Simulink models with VDM requirement specification.
Bug reporting for VDMTools bugs
Nothing to report, no bug report from Europe.
There are some bugs in version 8.0.1b-070820, and dr.k has fixed, but he didn’t uploaded it yet.


Status of Thomas’ work on the Overture type checker
Thomas will be asked to report on wiki.
Status of Hugo’s work on the Overture interpreter
Work is finished. The interpreter runs for some cases but further development need to be carried on. The interpreter wiki page will contain the information needed for the continuation.
Status of Sander’s work on the Overture proof support
Sander had network problems, so nothing to report.
The MONDEX case study
Latest report from Jeremy at The VDM Mondex Page. We are progressing slowly but things have moved forward in the last couple of weeks since John gave a proof tutorial. John is giving much more time to this in order to move things forward. Our goal is to have a Technical Report on Mondex by November and to try to give a paper on Mondex at the GC6 workshop proposed for FM’08.


John converted the VDM-SL article to interchange syntax and corrected it in a few places (more corrections may be needed). He also updated the general VDM article, which was mostly about reification. The two articles have been merged and the VDM-SL article now auto-redirects to VDM. Most “double redirects” have been eliminated. References have been updated.

The merged article now requires considerable smoothing plus:

This is wikipedia, so of course anyone is welcome to make additions and updates. Peter agreed to provide material on tool support and industry usage while John’s next job is to cut down the language description to just a discussion of the interesting features.

Anyone is welcome to contribute. If you plan any major changes, let John know so that duplication of effort can be avoided.

Publication Plans

In preparation:

In review:

In press:

Recently Appeared:

Other Business

Grand Challenges
We will have a regular agenda item on Grand Challenges (Mondex, Posix file store, Pacemaker) in future. This is not specifically part of VDMTools or Overture but is part of the Strategic Research Agenda.

: We will look for a champion to progress work on the Posix File Store challenge . John F will contact Jose (who has had some students working in the area) an also look for support on the vdm-forum mailing list.

: GC6 is planning a series of Grand Challenge workshops. Current proposals are: 1. An introductory workshop on the Posix challenge adjacent to the ICFEM 2007 conference. Jim made a proposal to the organisers of ICFEM (November 2007, Miami, USA) to run an introductory workshop on the Posix file store. We are waiting for the response. If this goes ahead, John will likely attend the event (rather than go to HASE’07 in Dallas where Peter is giving the traces paper). 2. A workshop adjacent to the BCS-FACS Christmas meeting. Jim has not made progress on that but has asked if John would get involved in organising it. John will approach BCS-FACS (Paul Boca and Jonathan Bowen) to assess the feasibility of holding it the day after the FACS workshop. It is believed this workshop would also be an attempt to gather interest in the Posix File Store challenge. 3. FM’08: A series of four half-day workshops on GCs are to be proposed for the Monday & Tuesday before the Symposium proper. IJim hasn’t indicated submission dates but no answer yet.

VDM at FM’08
We agreed to aim to hold a workshop at FM’08. Shin and Peter will coordinate the production of the proposal to John Derrick by 18 November. We decided not to offer a tutorial.

Next Meeting

14 October 2007, 1300 CET