Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

Net Meeting 25

Date 20 April 2008, 1300 CET
Participants Peter Gorm Larsen, JohnFitzgerald, Carlos Vilhena, Adriana Santos, Hugo Macedo, Shin Sahara, MarcelVerhoef, Augusto Ribeiro, SanderVermolen and Miguel Ferreira

Review of Action List

The actions are all at Overture on SourceForge.


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


Overture Parser Update
Marcel plans to release ASTGEN and the new parser ASAP. The interface to the AST classes have not changed, so it should work with the existing tools, like Sanders.
Status of Adriana’s work on the Overture Test Automation Support
Adriana specified the Combinatorial Testing Strategy. She is able to generate test cases based on Regular Expressions The filtering process is also specified, but at the moment the operation which tells if a test case had failed or not is fictitious… all test cases fail. Adriana will have to connect my specification with the VDMTools interpreter. The VDMTools interpreter will be used to run each test case and let know if the test case failed or not. If someone wants a more detailed description about something, please let her know.
Status of Carlos’ work on the Overture Connector between VDM++ and JML
Carlos started recently the implementation of the connection between VDM++ and JML. Concurrently, he continued writing the theoretical differences between the two referred languages and the requirement specification of this connection. He is also exploring another possibility of using the current JML parser to extract the forest of Abstract Syntax Trees form JML input files. For this purpose, he will try to use the new JML tools set (JML4), which is an Eclipse-based tool set of JML. Together with the JML community, he will try to overrun this problem/challenge. However, this will need further research about the limitations of the new tool set that they are developing.
Status of Augusto’s work on the Overture Proof Obligation Generator
Augusto is currently specifying the POG for the Termination Proofs. Method for discharge of this PO are also being studied, especially nested recursion.
Possible new students to take new Overture tasks
Peter will I try to contact José for potential new students who might be interested. Two new Danish MSc thesis students will work on Overture UML mapping after summer. New UK MSc student working from now to end August.
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.

Meeting with McMaster? people on FM’08

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. Miguel and Samuel are working on a Intel specification of the Flash File System Core.

Publication plans

In preparation:

In review:

In press:

Recently Appeared:

Strategic Research Agenda and Wikipedia

Peter has worked on Wikipedia entry and it had considerably improved. Feedback from potential readers would be important.

Any other business

Nothing to report.

Next Meeting

8 June 2008, 1300 CET