Net Meeting 19
||8 July 2007, 1300 CET
||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: Thomas have uploaded a zip file.
- 15/3 Ongoing.
- 15/4 Ongoing.
- 16/1 Ongoing.
- Status and development plans for VDMTools version 8.xx
- Currently released 8.0 RC version including VICE, this version fixed
many small bugs from IFAD era.
- The VDM team got 2 new VDM users. The jobs still small, but we think
this is the important step for VDM.
- Bug reporting for VDMTools bugs
- Fixed all bugs reported in English.
- Seminar at the end of July in Japan
- On 23rd and 24th July, VDM seminars will be hold in Tokyo and
Nagoya. Peter, Marcel and Shin are speakers.
- Status of Thomas’ work on the Overture type checker
- Thesis now defended successfully with the Danish mark 10.
- Status of Hugo’s work on the Overture interpreter
- Studies on the requirements the interpreter need to fulfill in order
to use Eclipse as an interface were done and on what’s the amount of
effort to be done in the Eclipse side.
- The conclusions so far are that it would be good to extend the
specification of the interpreter and thus implementation to add
functionality required by Eclipse GUI.
- Status of Sander’s work on the Overture proof support
- Sander is writing his thesis and have not developed anything anymore
since he left Denmark. The estimate on how much it is possible to
prove is above 60%, from that point on. In the writing pauses Sander
will try to apply the tool to the RTRI and Pacemaker examples and
report on the amount of proof that can be automated.
- The MONDEX case study
- Two mornings (15th and 22nd August) are planned to work on
refinement between the Abstract and Concrete models. These will
begin with a short tutorial on proof by John.
- The Pacemaker case study
- Marcel reported that Tom Maibaum is the professor from McMaster that
has adopted the PACEMAKER case for the GC6 initiative and they are
working (with Brian Larson) on setting up an initiative in north
America for certifying this kind of applications. Basically, the
Food and Drug Administration will make a standard to which all these
kind of devices shall conform.
- A workshop at FM’08 is planned as a side event for FM’08 aiming to
assess how first responses to the pacemaker challenge would look
like when trying to conform to this draft standard.
- With the work done so far we are on the edge and we should try to be
involved in the workshop planned to FM’08.
- We decided to try Sander’s work to prove part of Hugo’s PACEMAKER.
- New students from Minho for Overture
- Currently the new students are planning to work on
- Test automation
- JML coupling
- Paper path case study (Marcel)
- PhD thesis (Marcel)
- MSc Thesis (Hugo)
- MSc Thesis (Sander)
- Pacemaker modelling & validation (Hugo leading, Peter, John)
- Paper about proof work (Sander leading)
- Ways of handling Equality in LPF (John and Cliff) for IPL
- Traces Paper (John, Peter, Simon, Marcel), submitted to HASE07
- Encyclopedia of Computer Science & Engineering entry on “VDM” (John,
- Learning by Doing (John, Peter), submitted to FACJ special issue on
- Formal models of access control in XACML (Jeremy,John) accepted by
- Trading off Effort and Insight (Peter, John), to apear in Proc.
- Triumphs & Challenges for Lightweight Apps of M-O FMs (John, Peter,
keynote) in Proc Isola 2006 (IEEE proc., but no response from
editors on publication date yet).
- Dynamic Coalitions (Jeremy, John) in Proc. Isola 2006 (IEEE proc.,
but no response from editors on publication date yet)
- The LPF and VDM (John) in Dines and Martin Henson’s new book (with
Springer, estimated release 8 November).
- IFM Paper (Marcel et al.)
- DSN Fast Abstracts (Zoe, Marcel, John, Jeremy)
26 Aug 1300 CET