Net Meeting 19

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.

VDMTools

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.

Overture

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

Publication plans

In preparation:

• 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

In review:

• Traces Paper (John, Peter, Simon, Marcel), submitted to HASE07
• Encyclopedia of Computer Science & Engineering entry on “VDM” (John, Peter, Marcel)
• Learning by Doing (John, Peter), submitted to FACJ special issue on education

In press:

• Formal models of access control in XACML (Jeremy,John) accepted by ICFEM 2007
• Trading off Effort and Insight (Peter, John), to apear in Proc. Dines’ Festschrift
• 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).

Recently Appeared:

• IFM Paper (Marcel et al.)
• DSN Fast Abstracts (Zoe, Marcel, John, Jeremy)

Next Meeting

26 Aug 1300 CET