Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

Net Meeting 45

Date 25 July 2010, 1300 CET
Participants Peter Gorm Larsen, Shin Sahara, Hiroshi Sako, Kenneth Lausdahl, Augusto Ribeiro, Nick Battle, Nico Plat, (7 persons)

Review of Action List


See detailed report of Shin Sahara (sent to the overture-core mailing list) on the latest and greatest on VDMTools from Japan. AIST in Japan have had very impressive results using VDM++ for a commercial application.



Kenneth and Augusto have worked on a number of changes to the interpreter to handle VDM-RT in debug mode, this is not finished but now it can run debugging but still requires lots of resources. Other things include a better outline, debug interface with deep variable inspection and change highlights etc. Self update and the normal update manager have also been enabled. A new 0.3 RC is now available at SF and it needs to be tested by all Overture stakeholders.


Updated with a thread pool to limit resource usage in VDM-RT model with a large number of short living threads (Async and Periodic). To ensure that VDMJ is deterministic, automated test scripts have been made to execute models on batch mode both command line and through the debug interface.


The minutes of the language board were briefly discussed. The status of the upcoming Overture workshop on semantics (13 september at London) was briefly discussed.

Publication plans

See Planned Publications (page has been updated). The Japanese translation of the Validated Designs book is due in bookstores at the beginning of August.

Any Other Business

Moving things over to the new wiki was briefly discussed.

Next Meeting

Next meeting is due on Sunday 22 August, 13h00 CET.