Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

Net Meeting 15

Date 4 February 2007, 1200 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.


Status of VDMTools development
Shin reported that CSK has opened a VDMTools subversion source repository: https://www.vdmtools.jp/svn/vdmtools/ It is free of charge, but you have to sign a following non disclosure agreement with CSK Systems before accessing the repository. Peter and Marcel had used the SVN reporsitory successfully.
Bug reporting for VDMTools bugs
Nothing to report at present.


Parser movedto Sourceforce and testing of it
Estimate moving the parser to sourceforge on 1 April. The wiki distribution is sufficient for current purposes. Any problems with the parser can be addressed on demand by Marcel (by email in the first instance).
Status of Thomas’ work on the Overture type checker
Peter had no explicit status message regarding the static semantics but understands that Thomas is almost finished with the subset that he will be able to cover. He needs then to write up the actual thesis. The Static Semantics should go into Sourceforge, along with the parser.
Welcome to Hugo and Sander starting their MSc thesis work on Overture
We welcomed Hugo and Sander!
More potential projects for Overture
Discussed already.
Structure of future Overture research
John has agreed to make a pass over the There is a Strategic Research Agenda (SRA) wiki topic at vdmportal.org.

: At 3rd Overture Workshop in Newcastle we agreed to try to develop and maintain a Strategic Research Agenda. This is a sort of guide that will allow people to easily join us and select cool research topics to address and write papers about etc. It also allows us to ensure coverage of important core concepts so that we do not end up with rather patchy research with some core areas not addressed. We agreed to structure research activity into three strands of work: Semantics; Methods & Applications and Tools. For example, Hugo’s work will largely fit within the Tools strand.

: Cutting across the three strands of research, we will have Challenges. These are focussed specific problems that bring together research in several areas and allows us to see our progress and also allows us to test out developments. The three main challenges under consideration at the moment are “Mondex”, “Pacemaker” and “Posix”.

: John proposes that the SRA page should evolve by the lead contacts in each stream or challenge soliciting brainstorm lists of open research problems in their area, as well as identifying important base research that should be done in order to provide a suitable platform. For example, in Semantics, John will have “Denotational Semantics of VDM++” as a base topic and “Can we adequately represent LPF in HOL” as an open question. As an example of a challenge, Marcel could propose a specific problem arising out of his doctoral work, such as modelling and analysis of a photocopier controller.

Mondex and Pacemaker case studies

Our first challenge is Mondex - an electronic purse system specified and designed via data refinement originally in Z. Several people have expressed interest in tackling Mondex in VDM. This work is being led by Jeremy Bryans at Newcastle. A workshop is scheduled for 2-3 April at Newcastle for the interested people to make concrete progress. Prior to that, a reading group at Newcastle will review the monograph that describes the Mondex study in Z.

The Pacemaker study has now been released and we need to find a champion within the Overture community. It was suggested that CSR Newcastle could again take the lead, with Zoe Andrews contributing, as the application lends itself well to the work that Marcel and Zoe have been doing on stochastic fault modelling. It’s also Zoe’s potential PhD topic, which John would supervise.

Any Other Business

John suggested having a discussion of publication status and plans as a regular topic in Overture net meetings.

Next Meeting

4 March 2007 1200 CET