Net Meeting 35

Review of Action List

The actions are all at Overture on SourceForge.

• 24/4: Find out about Rodin Tool plug-in standards - Closed
• 33/1: ALL to comment on proposed logos - Closed
• 33/3: Kenneth update Ov. wiki and set up tools updatesite - Development guide is missing, Carried forward
• 34/1: Shin to enable everyone to see tracking - Carried forward
• 34/2: PGL create email list for LB - Closed
• 34/3: All to update web pages - Carried forward

VDMTools

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

Overture

Status for each of the Overture components at sourceforge

traces (Peter)

It was discovered that the specification in VDM which is code generated does not scale very well when looking at tests in the range of half a million to a million. Because of this problem it has been chosen to change the core of the traces to use the VDMJ traces feature.

eclipse (Christian and David)

The editor was built and an update site has been uploaded to overture.org together with a pre-installed Eclipse for Windows a discussed in Newcastle at the workshop. Overture Sourceforge

The development environment has been described in a similar style on Developer_Documentation where it’s possible to install all tools manual or download an Eclipse for Windows / Linux which is pre-installed. The DLTK problem discovered in Newcastle has been solved by taking a snapshot of the DLTK update site and uploading it to overture.org.

POTrans (Miguel)

Since the last workshop Miguel was able to tryout some ideas some of you provided ffor the interaction between the potrans component and HOL. Although the solution isn’t perfect yet, some progress has been made.

VDMJ (Nick)

Some of the language proposals where implemented though they can be backed out if not accepted. Several bugs have been corrected.

Overture Community Process

Note: Language Board = Executive Committee.

The LB accepted the first three proposals and they are:

• International character support for Overture identifiers
• The introduction of the “reverse” sequence operator
• Generalising let-be expressions

Nick was proposed to be Secretary of the LB.

Overture Version

Two version of the release are available, one for developers and another for users.

Workshop

Sony will give an invited talk at the next workshop

Publication plans

In preparation:

• Overture Introductory paper aimed at ACM SE Notes (Peter, John, others?)
• Paper path case study (Marcel & Jozef)
• New proof paper (Sander, Peter, Augusto, Jozef)
• CT (Kenneth, Peter)
• Japanese Translation of VDM++ Book (Sakoh, hopefully publication by August 2009)

In review:

• UML mapper (Kenneth, HK, Peter) submitted to FM’09
• Pos for Recursive Functions (Augusto, Peter) submitted to FM’09
• ACM Computing Surveys paper on industrial applications of FMs (Jim, Peter, Juan, John): very last stages of preparation now. Well received.
• VICE Process paper (John, Peter, Sune Wolff) submitted to special issue of International Journal of Software and Informatics
• Felica (Mr Kurita and maybe Shin?) submitted to special issue of International Journal of Software and Informatics.

In press:

• Jozef and Marcel: Formal Semantics of a VDM Extension for Distributed Embedded Systems; to appear in Festschrift for W P de Roever (LNCS).
• Jozef, A summary of the FM06 and IFM07 paper and enhanced the PVS models, to appear in Festschrift for W P de Roever (LNCS).

Recently appeared (since last NM):

• 2nd edition of “Modelling Systems”, Cambridge University Press (John & Peter). Link

Any Other Business

None.

Next Meeting

August 2nd 2009, 1300 CET

Note: next NM should address the problem of 13:00 CET = 20:00 JST.