Net Meeting 40

Review of Action List

The actions are all at Overture on SourceForge.

• 38/2: still open. As indicated at the last NM, Marcel and John will address this later in January when they are together in Twente in late january.

VDMTools

Shin sent out the usual VDMTools report (see overture-core list).

Overture

Status for each of the Overture components at sourceforge

traces

Traces: We are still working on the paper and have made some minor bug fixes.

Overture IDE

• The new feature of VDM-10 have been made available through a property tab on a project.
• New launch tab has been made. Now there is no need to select a file name anymore, just the class/ module and operation/function. Here a number of bugs has been fixed. E.g. starting the debugger with a string argument for an operation.
• The debug launcher now takes a argument for memory in the overture.ini into account when starting so we can increase the memory allowed for the debug virtual machine.
• A coverage option has been added to the launch configuration and will soon be available when running a VDM model. VDMJ already includes all the information.
• A small test feature has been added to the Overture debug helper plug-in to enable generation of latex – pdf document of a model.
• PO Viewer: Here the GUI has been upgraded so it keeps the same numbering even when the filter option is enabled. Additional bug fixes has also been made.

Overture Language Board

Only Peter and Nick have stated their wish to be re-elected. Nick will work on re-establishing the LB for the next NM. Action 40/1.

• Release Policy

Nick suggested that release policy should be managed via the LB via “issues” - except for the third-digit builds. There is always an outstanding release “issue”, and developers working to implement it.

Action (40/2) on Peter to coordinate a release plan that has the support of core members and DESTECS. He can start this during the DESTECS Kick-off but it will have to be discussed with core before being agreed.

Publication plans

Planned (note the lead author and approximate date):

• DESTECS paper on static correctness conditions for co-simulation (John, June 2010)
• DESTECS paper on co-simulation incl. tool support (Peter, end 2010, aiming for FM’11)
• DESTECS paper on case studies (Marcel, aiming for an I-Day in 2010 or 2011)
• DESTECS paper on fault modelling in VDM and in co-sim framework (John, 2011)

In preparation:

• Paper path case study (Marcel & Jozef, target end January 2010) for Journal of Systems and Software
• Japanese Translation of VDM++ Book (Sako)
• POs for Recursive Functions (Augusto, Peter)
• CT (Kenneth, Peter, Nick)
• DESTECS project introduction (Peter, Jan Broenink, Marcel, et al., due January 2010)

In review:

• None

In press:

• Overture Introductory paper aimed at ACM SE Notes (Peter, Nick, Miguel, John, Kenneth, Marcel) – due January 2010.
• New proof paper (Sander, Peter, Jozef) accepted to SAC
• Formal Semantics of a VDM Extension for Distributed Embedded Systems (Jozef and Marcel) in Festschrift for W P de Roever (LNCS 5930) – due January 2010.

Recently Appeared:

• None

EVERYONE please remember to update the publications list on vdmportal.org

EVERYONE please remember to acknowledge DESTECS in any relevant publications!

Any Other Business

Overture Documentation

• Three Overture tool introductions have been prepared for the 3 dialects, each as a replacement Chapter 3. We’ll get reviews of the draft chapters from colleagues.
• A guide to Overture for potential adopters: Actions 40/3 and 40/4 - Peter and Nick to review older VDM marketing materials.

Next Meeting

6 February 2010, 1500 CET