Net Meeting 17
||14 April 2007, 1300 CET
||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.
- 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:
Mail address for questions about bugs is: email@example.com Not
yet decided upon possibility for users to see the status of the bugs
that have been reported
- 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
- 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
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.
- Traces Paper (John, Peter, Simon, Marcel), now due 14 April.
- The Goldsmith Conjecture and LPF (John, Cliff) now due end April for
- Paper path case study (Marcel) for SCSC (a leading simulation
- 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.
- 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.
- 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
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.
20 May 1300 CET