Net Meeting 43

Review of Action List

The actions are all at Overture on SourceForge.

• 38/2: still open. This action is being carried forward.
• 39/1: still open. This action is being carried forward.
• 41/1: still open. This action is being carried forward.
• 41/3: still open. This action is being carried forward.
• 42/1: open: suggestions needed for speakers for each block of the september workshop (by e-mail to Nico).

VDMTools

Shin sent out the usual VDMTools report (see overture-core list). Functions are now static in VdmTools?.

Overture

VDMJ

Status mail sent by Nick.

ASTGen

Marcel have been working on a new version of the ASTGen he hope he will be able to release it very soon for testing.

Overture IDE

Status mail sent by Kenneth and Augusto. Since the last meeting we have progressed and just been able to make a very first internal test version of the new IDE. This version includes most of the features from the current release 0.2 but still no plug-ins (latex, PO Viewer, UML Trans etc). which we have assessed to be fairly easy to upgrade.

Overture Language Board

The following language issues are “open” at the moment: - VDM++ Object oriented issues. A wide collection of issues which have been stalled because the lack of language semantics documentation. However, these issues will be subject of discussion during the Overture Workshop in September. - Invariant functions for record types. Here the LB has reached a decision and the RM has now been moved to the “Discussion” Phase of the OCP, which effectively means it should be discussed buy the Overture Community at large. - Exception handling in interpreter. This RM has been discussed by the LB but no decision has been reached yet. Most likely discussion will be restarted following the procedures of the LBP (in a “fasttrack” way)..

Release status of Overture IDE 0.2

Shin has been testing the IDE with Japan models written in Shift-JIS and discovered strange conversions between Shift-JIS and UTF-8. He will mail example model to Kenneth Lausdahl.

Marcel raised a question about what should be included of external plug-ins in the release (SVN/CVS) which lead to a longer discussion about how to decide which plug-ins goes into the release.

The discussion will continue offline but Nico raised the concern that we should see if we could improve the procedure which is used to specify what goes into the release.

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)
• Paper on the jmltrans tool (Peter and Carlos)
• Co-simulation examples (John and Ken)
• Pacemaker Challenge state of the art (John et al.)
• Interpreter and Deterministic Scheduling (Kenneth, with Nick, Marcel and Peter, aiming for end of 2010 possibly for FACJ)

In preparation:

• Paper path case study (Marcel & Jozef, target end February 2010) for Journal of Systems and Software
• Japanese Translation of VDM++ Book (Sako) Target end March
• POs for Recursive Functions (Augusto, Peter)
• Abstraction (Jens, Peter, John)

In review:

• CT (Kenneth, Peter, Nick, submitted to SEFM, feedback due in May)

In press:

• DESTECS project introduction (Peter, Jan Broenink, Marcel, et al.)

Recently Appeared:

• Overture Introductory paper aimed at ACM SE Notes (Peter, Nick, Miguel, John, Kenneth, Marcel)
• 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)

Any Other Business

SEMAT (suggested by NB): SEMAT (Software Engineering Method and Theory) is an initiative to reshape Software Engineering such that Software Engineering qualifies as a rigorous discipline. The initiative was launched in October 2009. It’s interesting for several reasons: it obviously relates to the formal modelling we aspire to with Overture; it has a very impressive list of signatories, including Dines Bjorner; their presentation material has already started talking about formal methods and VDM in particular; and (most unusual of all) I found out about this via Fujitsu (UK), who are a corporate signatory, and whose tools group is interested in the initiative.

September workshop: suggestions needed for speakers for each block by e-mail.

Next Meeting

To be doodled.