Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

Net Meeting 17

Date 14 April 2007, 1300 CET
Participants John Fitzgerald, Peter Gorm Larsen, Hugo Macedo, Shin Sahara, Marcel Verhoef, Sander Vermolen

Review of Action List

The actions are all at Overture on SourceForge.

Mail address for questions about bugs is: bug_report@vdmtools.jp Not yet decided upon possibility for users to see the status of the bugs that have been reported


Status of VDMTools development and the CSK VDM development team
Shin reports that the focus next year is to get customers. Then to decide on features during the job training. They have 4 candidate users And, will get 3 VDM engineers from out of CSK.
Bug reporting for VDMTools bugs
Peter expresses his concern about the statement that the Rose link does not work. Shin does not know the details yet. Discussion postponed.


Status of Thomas’ work on the Overture type checker
Unknown how far Thomas is, but considering that he has to hand in his thesis by the 30th of April, the SS should be uploaded within a couple of weeks.
Status of Hugo’s work on the Overture interpreter
Finishing (debugging) the legacy evaluator aproach. Plans once the legacy version is finished are:
  • Try to measure its performance and
  • Develop ideas on the Java interpreter (the alternative where JVM is used for interpreting VDM instructions directly).
  • The translation between Oml AST and AS is the main problem Hugo is still working on w.r.t. porting the interpreter.
Status of Sander’s work on the Overture proof support
On the status report Peter comments that OO support and explicit operations are not trivial. John suggests to take a look at the abstract spec of the Mondex case study, which will be good to work on next time Sander visits Newcastle. John will send the abstract specs after a quick walkthrough next week.
Mondex and Pacemaker case studies
John explains that they are using the Mondex study to involve more people in Newcastle in VDM and increase skills in VDM++. So far the abstract and concrete models are developed and they’re starting the refinement proof after this week. Peter agrees to Marcel to send an email to their contact in the US, informing that they are starting with it.

Publication plans

Peter mentions they have a paper to be submitted tomorrow. About formulating validation conjectures over execution traces.

Marcel has just delivered the final version of the IFM paper It has improved as well, due to the review comments. He has also made the following arrangement with Chess: April is used for FP7 related work. May is for the final touch on his thesis. June 1: really start working for Chess again.

In preparation:

In review:

In press:

Any Other Business

Marcel mentions there is a student at TU Delft who is using the Overture parser (via Cees Pronk) translating VDM++ models to Lydia a language for dependability analysis Agreed to have a workshop in December and one at FM08. The first more dedicated on GC, Sander and Hugo’s work. Marcel will be general chair in December.

Next Meeting

20 May 1300 CET