Record of Overture NM20, 26 August 2007, 1300 CET

Participants: John Fitzgerald,Peter Gorm Larsen, Hugo Macedo, Shin Sahara, Emma Nicholls

Review of Action List

The actions are all at Overture on SourceForge.

13/2 Ongoing: Waiting for new participants.

15/2 Ongoing: Thomas is going to write the wiki about the TypeCheker^?.

15/3 Closed.

15/4 Closed.

16/1 Ongoing.

VDMTools

Status and development plans for VDMTools version 8.xx

Shin reported the development plan in this year is:

• make VDM++TesK like test case generator prototype

http://www.ispras.ru/~RedVerst/RedVerst/White%20Papers/vdmtesk/Main.html

• make BIT, BYTE class as standard library

Functionality required by an important customer.

Actually trying to get the third user from the embedded system world, the important point is how to write a requirement specification for embedded systems. And, important point in the near future is how to connect Simulink models with VDM requirement specification.

Bug reporting for VDMTools bugs

Nothing to report, no bug report from Europe.

There are some bugs in version 8.0.1b-070820, and dr.k has fixed, but he didn't uploaded it yet.

Overture

Status of Thomas' work on the Overture type checker

Thomas will be asked to report on wiki.

Status of Hugo's work on the Overture interpreter

Work is finished. The interpreter runs for some cases but further development need to be carried on. The interpreter wiki page will contain the information needed for the continuation.

Status of Sander's work on the Overture proof support

Sander had network problems, so nothing to report.

The MONDEX case study

Latest report from Jeremy at The VDM Mondex Page. We are progressing slowly but things have moved forward in the last couple of weeks since John gave a proof tutorial. John is giving much more time to this in order to move things forward. Our goal is to have a Technical Report on Mondex by November and to try to give a paper on Mondex at the GC6 workshop proposed for FM'08.

The Pacemaker case study

Emma has been building a validation GUI for the pacemaker models in Java. Currently it will allow the execution of any valid scenario on any of the pacemaker models and displays the results on a basic graphical trace, with vertical lines representing pulses. Some small changes were required to the model to allow this, mostly consisting of the addition of a returnResult() method to each Environment to allow the return of data rather than just the printing of it.

Wikipedia

John converted the VDM-SL article to interchange syntax and corrected it in a few places (more corrections may be needed). He also updated the general VDM article, which was mostly about reification. The two articles have been merged and the VDM-SL article now auto-redirects to VDM. Most "double redirects" have been eliminated. References have been updated.

The merged article now requires considerable smoothing plus:

• Removal of VDM-SL detail that is already in the textbooks.
• Writing more interesting material on the particular features of VDM
• Addition of material on the tools and industrial use
• Addition of further external links and references.

This is wikipedia, so of course anyone is welcome to make additions and updates. Peter agreed to provide material on tool support and industry usage while John's next job is to cut down the language description to just a discussion of the interesting features.

Anyone is welcome to contribute. If you plan any major changes, let John know so that duplication of effort can be avoided.

Publication plans

In preparation:

• Paper path case study (Marcel)
• PhD thesis (Marcel)
• MSc Thesis (Hugo)
• Pacemaker modelling & validation (Hugo leading, Peter, John)
• Paper about proof work (Sander leading)
• Ways of handling Equality in LPF (John and Cliff) for IPL
• ACM Computing Surveys paper on industrial applications of FMs (Peter, Juan, John)
• New Wikipedia entry on “VDM”, replacing current separate entries on VDM and VDM-SL. (John)
• FeliCa^? paper (Araki, Peter and FeliCa^?)
• 2nd edition of "Modelling Systems", Cambridge University Press (John & Peter)

In review:

• Wiley Encyclopedia of Computer Science & Engineering entry on "VDM" (John, Peter, Marcel)
• "Learning by Doing" (John, Peter), submitted to FACJ special issue on education
• "The Connection between Two Ways of Reasoning about Partial Functions" (John and Cliff), submitted to Information Processing Letters

In press:

• 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 in dynamic coalitions (Jeremy and John) to Pro-VE 2007
• "Balancing Insight and Effort: the Industrial Uptake of Formal Methods" (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

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

Other Business

Grand Challenges

We will have a regular agenda item on Grand Challenges (Mondex, Posix file store, Pacemaker) in future. This is not specifically part of VDMTools or Overture but is part of the Strategic Research Agenda.

We will look for a champion to progress work on the Posix File Store challenge . John F will contact Jose (who has had some students working in the area) an also look for support on the vdm-forum mailing list.

GC6 is planning a series of Grand Challenge workshops. Current proposals are:

1. An introductory workshop on the Posix challenge adjacent to the ICFEM 2007 conference. Jim made a proposal to the organisers of ICFEM (November 2007, Miami, USA) to run an introductory workshop on the Posix file store. We are waiting for the response. If this goes ahead, John will likely attend the event (rather than go to HASE'07 in Dallas where Peter is giving the traces paper).
2. A workshop adjacent to the BCS-FACS Christmas meeting. Jim has not made progress on that but has asked if John would get involved in organising it. John will approach BCS-FACS (Paul Boca and Jonathan Bowen) to assess the feasibility of holding it the day after the FACS workshop. It is believed this workshop would also be an attempt to gather interest in the Posix File Store challenge.
3. FM’08: A series of four half-day workshops on GCs are to be proposed for the Monday & Tuesday before the Symposium proper. IJim hasn't indicated submission dates but no answer yet.

VDM at FM'08

We agreed to aim to hold a workshop at FM'08. Shin and Peter will coordinate the production of the proposal to John Derrick by 18 November. We decided not to offer a tutorial.

Next Meeting

14 October 2007, 1300 CET

-- HugoMacedo - 28 Aug 2007