Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

Net Meeting 24

   
Date 16 March 2008, 1400 CET
Participants Peter Gorm Larsen, JohnFitzgerald, Carlos Vilhena, Adriana Santos, Hugo Macedo, Shin Sahara, MarcelVerhoef, Augusto Ribeiro and SanderVermolen

Review of Action List

The actions are all at Overture on SourceForge.

VDMTools

Status and development plans for VDMTools version 8.xx
Version 8.1 is now available.

Overture

Status of Adriana’s work on the Overture Test Automation Support
Adriana is starting implementing a combinatorial testing tool for VDM++, based on Tobias Tool. She also wrote a theoretical approach for Mutation Testing in VDM++. A Mutation Testing Tool will not be implemented due to insufficient resources on the Overture.
Status of Carlos’ work on the Overture Connector between VDM++ and JML
Carlos overrun all the major theoretical details that kept him for starting the implementation of the connection between JML and VDM++. He will now start implementing the tool.
Status of Augusto’s work on the Overture Proof Obligation Generator
Augusto is trying to find a way of proving function termination automatically, including nested functions.
Possible new students to take new Overture tasks
Peter will I try to contact José for potential new students who might be interested.
The MONDEX case study
They started this work by concentrating on illustrative proofs of correct refinement. There has been slow progress because it all has to be done by hand. One can see the state of the proof checking on the Wiki page. They still plan to generate a TR including the proofs. However, they have decided to make a main focus the illustration of test-based validation technology using VDMTools (so far the main distinctive selling point of VDM). To that end, Ken has been involved in setting up a testing framework which is now installed in a local SVN repository (along with the emerging TR).
John thinks they can get there in the end but, because this has not been a concentrated effort (because of lack of willingness to commit concentrated resources) it will not tell an encouraging story about VDM. Their lack of proof tools is still a major weakness compared to other formalisms. However, their testing support is impressive. The work has had a beneficial effect in spreading experience in VDM, VDMTools and proof among a wider group here in Newcastle.
The Pacemaker case study
Hugo has so far made the one serious attempt at this study. The models were a good start, but they were mainly developed in order to illustrate a development methodology rather than to make a significant attack on the pacemaker study. Zoe has been looking in detail at some of the models (and indeed is now attempting them in Event-B) and feels that major revisions would be required if they were attempting a serious attack on the study. John’s main concern is that there is no definite specification of what the challenge problem is and, further, how anyone can attempt it without access to domain expertise. For the moment, this remains an example used to illustrate other things. John sees no prospect of that changing unless more people than himself and Zoe commit time and resources, and they get some domain expertise.
The POSIX
John will update to the BTrees model that has been adopted into the study by Jim Woodcock, based on some old VDM work. José Nuno has a small team working in this area and they are also in contact with Sander.

Publication plans

In preparation:

In review:

In press:

Recently Appeared:

Any other business

Nothing to report.

Next Meeting

20 April 2008, 1300 CET