Net Meeting 21

Review of Action List

The actions are all at Overture on SourceForge.

• 13/2 Ongoing: Ken Pierce has taken it over.
• 15/2 Ongoing: Thomas is going to write the wiki about the TypeCheker.
• 16/1 Ongoing.
• 20/1 Closed.
• 20/2 Ongoing: Hugo is going to upload PACEMAKER report information.
• 20/3 Ongoing: Need contributions on modules and classes.
• 20/4 Closed.
• 20/5 Ongoing.

VDMTools

Status and development plans for VDMTools version 8.xx

The VDMTools newest version is 8.0.1b-071011 with some small bugs fixed. A part of interpreter code was rewritten for efficiency.

There are two new users. Both are still small jobs, one decided to use VDM as a detail design specification language. The other requires a report on “How to write requirement specification”. The problem is how to make the requirement specification for plant model (physical model) and control software.

Bug reporting for VDMTools bugs

All bugs reported in English were fixed.

Overture

Status of Thomas’ work on the Overture type checker

Nothing to report.

Status of Hugo’s work on the Overture interpreter

Hugo will add status information and update the wiki with his technical report.

Status of Sander’s work on the Overture proof support

Sander is to update the wiki according to the VDMTools Proof Obligation generation new features (file output).

The MONDEX case study

Latest report from John is that there is steady progress and some interesting refinement issues have been identified. Current plan is prepare a paper for the FM08 Grand Challenge workshops (which may then transform into a journal paper).

The Pacemaker case study

Hugo is to upload his thesis after defense and Emma’s thesis was approved this week.

Introduction to new Overture subjects (Adriana, Carlos and Augusto)

Carlos is starting his thesis: “Connecting between VDM++ and JML” . Now reading some material to get into this theme, while modelling the “Alarm System” in JML in order to compare the differences between JML and VDM++.

Adriana is working on test automation support. Now reading about the different ways to make test automation and trying to run the VDMTesk tool.

Publication plans

In preparation:

• Paper path case study (Marcel)
• PhD thesis (Marcel)
• Pacemaker modelling & validation (Hugo, Peter, John)
• Paper about proof work (Sander)
• ACM Computing Surveys paper on industrial applications of FMs (Peter, Juan, John)
• FeliCa paper (Araki, Peter and FeliCa)
• 2nd edition of “Modelling Systems”, Cambridge University Press (John & Peter) by end 2007

In review:

• Wiley Encyclopedia of Computer Science & Engineering entry on “VDM” (John, Peter, Marcel) - review comments have been promised imminently
• “The Connection between Two Ways of Reasoning about Partial Functions” (John and Cliff), submitted to Information Processing Letters
• MSc Thesis (Hugo)

In press:

• New Wikipedia entry on “VDM”, replacing current separate entries on VDM and VDM-SL. (John)
• “Learning by Doing” (John, Peter, Steve Riddle), submitted to FACJ special issue on education
• Traces Paper (John, Peter, Simon, Marcel), accepted by HASE07
• Formal models of access control in XACML (Jeremy,John) accepted by ICFEM 2007
• Workshop submission on visualizing models of access control

Recently Appeared:

• “Balancing Insight and Effort: the Industrial Uptake of Formal Methods” (Peter, John), to appear in Proc. Dines’ Festschrift
• MSc Thesis (Emma)

Strategic Research Agenda and Wikipedia

Peter updated http://www.vdmportal.org/twiki/bin/view/Main/SRA and feedback is welcome.

Wikipedia VDM section has been updated but still need improvements.

Any other business

Note that FM’09 will be in Eindhoven.

John also said, he is PC Chair for ICTAC 2008 and welcome suggestions for workshops or indeed papers for the conference. Also welcome are papers on the application of theories, especially in areas such as domain modelling; Also welcome are papers on support for theories in tools. There are likely to be a couple of special tracks, probably on domain modelling and tool support as the topics.

Next Meeting

18 November 2007, 1300 CET