The actions are all at Overture on SourceForge.
Cool new Eclipse features discovered recently
News about the rCOS tool
Overture Parser Update
Nothing to report.
Status of Adriana’s work on the Overture Test Automation Support
Adriana made the expanded version of the traces written by the user.
Status of Carlos’ work on the Overture Connector between VDM++ and JML
Carlos got the JML parser interacting with his mapper. He will continue mapping from VDM to JML in VDM++.
Status of Augusto’s work on the Overture Proof Obligation Generator
Augusto finished the implementation of the POG, apart from some minor things involving classes that are not working properly.
New students (Kenneth and Hans Christian)
Kenneth and Hans Christian will development a tool similar with Rose link from VDMTools. They will extend the overture project with an eclipse plugin (EMF) for going back and forth between VDM and UML. Additionally they will take a look at the test trace file and see if it is possible to pars this file into a UML sequence diagram.
The MONDEX case study
Jeremy and John have discussed a substantial paper on Mondex for FACJ with Jim Woodcock, who is planning a special issue on Mondex follow-up. The one thing John would like to show that was not done so far is a GUI for domain expert validation. John has a student who wants to work in this area but she is going to be part time and will take long. He is considering whether he can divert PhD? student resource on this at Newcastle.
The Pacemaker case study
Pacemaker FAQ is in the wiki at http://www.cas.mcmaster.ca/wiki/index.php/Pacemaker_FAQ The head of wiki is: http://www.cas.mcmaster.ca/wiki/index.php/Pacemaker John will give an invited talk on the pacemaker work as part of a GC day immediately preceding the ABZ conference in London in September. He will work further on Pacemaker before then.
Improvements were made in proving the proof obligations automatically in HOL. A vote of thanks to Hugo and Miguel is made for speaking at the GC workshop - it got the community a lot of good publicity and improved recognition in the GC community. They liked the way the community is using the challenges to explore and benchmark different aspects of the VDM technology. Miguel is preparing a page for the VDMPortal compiling all the material they have so far.
An Overture Summer School was suggested and it will be discussed in the next meeting. The members of the Overture community should take an action to investigate the rCOS plug-ins. A description of the rCos tool is available on http://rcos.iist.unu.edu/tool.
20 July 2008, 1300 CET