Net Meeting 17

Review of Action List

The actions are all at Overture on SourceForge.

• 13/2 Ongoing: Progressing as a by-product of the Mondex work.
• 15/2 Ongoing: Should be closed at the next NM
• 15/3 Ongoing: Have all been too bit busy to do this. Suggested to set a date for getting together on this point but after Marcel’s PHD submission and after FP7 close.
• 15/4 Ongoing: Same reason as above. Hugo is going to have a first go at a part of it in Peter’s VDM course
• 16/1 URL for bug reporting of VDMTools bugs is: http://www.vdmtools.jp/en/modules/bmsurvey/survey.php?name=Bug_report

Mail address for questions about bugs is: bug_report@vdmtools.jp Not yet decided upon possibility for users to see the status of the bugs that have been reported

VDMTools

Status of VDMTools development and the CSK VDM development team

Shin reports that the focus next year is to get customers. Then to decide on features during the job training. They have 4 candidate users And, will get 3 VDM engineers from out of CSK.

Bug reporting for VDMTools bugs

Peter expresses his concern about the statement that the Rose link does not work. Shin does not know the details yet. Discussion postponed.

Overture

Status of Thomas’ work on the Overture type checker

Unknown how far Thomas is, but considering that he has to hand in his thesis by the 30th of April, the SS should be uploaded within a couple of weeks.

Status of Hugo’s work on the Overture interpreter

Finishing (debugging) the legacy evaluator aproach. Plans once the legacy version is finished are:

• Try to measure its performance and
• Develop ideas on the Java interpreter (the alternative where JVM is used for interpreting VDM instructions directly).
• The translation between Oml AST and AS is the main problem Hugo is still working on w.r.t. porting the interpreter.

Status of Sander’s work on the Overture proof support

On the status report Peter comments that OO support and explicit operations are not trivial. John suggests to take a look at the abstract spec of the Mondex case study, which will be good to work on next time Sander visits Newcastle. John will send the abstract specs after a quick walkthrough next week.

Mondex and Pacemaker case studies

John explains that they are using the Mondex study to involve more people in Newcastle in VDM and increase skills in VDM++. So far the abstract and concrete models are developed and they’re starting the refinement proof after this week. Peter agrees to Marcel to send an email to their contact in the US, informing that they are starting with it.

Publication plans

Peter mentions they have a paper to be submitted tomorrow. About formulating validation conjectures over execution traces.

Marcel has just delivered the final version of the IFM paper It has improved as well, due to the review comments. He has also made the following arrangement with Chess: April is used for FP7 related work. May is for the final touch on his thesis. June 1: really start working for Chess again.

In preparation:

• Traces Paper (John, Peter, Simon, Marcel), now due 14 April.
• The Goldsmith Conjecture and LPF (John, Cliff) now due end April for IPL.
• Paper path case study (Marcel) for SCSC (a leading simulation conference).
• Encyclopedia of Computer Science & Engineering entry on “VDM” (John, Peter, Marcel) due 25 May
• Wikipedia entry on VDM (John) aiming for 25 May as well.
• Marcel’s thesis.
• PGL DB festschrift contribution.
• JSF DB festschrift contribution.

In review:

• Fast Abstracts for DSN 2007 (John, Jeremy, Zoe, Marcel). There is one (Jeremy & John) on VDM++ modelling in support of access control policy negotiation in dynamic coalitions and there is one (Zoe, John & Marcel) on fault modelling and simulation as an augmentation to the 20-SIM/VDMTools co-simulation environment.

In press:

• Water Tank case study (IFM)
• Isola keynote (John, Peter) in Isola proceedings (No response so far to two requests for publication date from editors).
• Dynamic Coalitions (Jeremy, John) in Isola proceedings (No response so far to two requests for publication date from editors).
• The LPF and VDM (John) in Dines and Martin Henson’s new book (with publisher).

Any Other Business

Marcel mentions there is a student at TU Delft who is using the Overture parser (via Cees Pronk) translating VDM++ models to Lydia a language for dependability analysis Agreed to have a workshop in December and one at FM08. The first more dedicated on GC, Sander and Hugo’s work. Marcel will be general chair in December.

Next Meeting

20 May 1300 CET