Net Meeting 15

Review of Action List

The actions are all at Overture on SourceForge.

• 9/10 Closed
• 10/2 Closed
• 13/2 remains open. John suggested that job could be done as a by-product of the Mondex challenge. He has contacted Jeremy Bryans (leading the Mondex challenge) to ask for this to be done.
• 14/1 Closed. The Third Overture Workshop was considered a success. Thanks to all those who contributed.
• 14/2 remains open. Discussed further when considering the research agenda.
• Action 15/1 (replaces unnumbered item on project descriptions): Project descriptions to go on overturetool.org (John) for subsequent extension (Peter)

VDMTools

Status of VDMTools development

Shin reported that CSK has opened a VDMTools subversion source repository: https://www.vdmtools.jp/svn/vdmtools/ It is free of charge, but you have to sign a following non disclosure agreement with CSK Systems before accessing the repository. Peter and Marcel had used the SVN reporsitory successfully.

Bug reporting for VDMTools bugs

Nothing to report at present.

Overture

Parser movedto Sourceforce and testing of it

Estimate moving the parser to sourceforge on 1 April. The wiki distribution is sufficient for current purposes. Any problems with the parser can be addressed on demand by Marcel (by email in the first instance).

Status of Thomas’ work on the Overture type checker

Peter had no explicit status message regarding the static semantics but understands that Thomas is almost finished with the subset that he will be able to cover. He needs then to write up the actual thesis. The Static Semantics should go into Sourceforge, along with the parser.

• Action 15/2: Thomas to place static semantics on Sourceforge (Peter)

Welcome to Hugo and Sander starting their MSc thesis work on Overture

We welcomed Hugo and Sander!

More potential projects for Overture

Discussed already.

Structure of future Overture research

John has agreed to make a pass over the There is a Strategic Research Agenda (SRA) wiki topic at vdmportal.org.

: At 3rd Overture Workshop in Newcastle we agreed to try to develop and maintain a Strategic Research Agenda. This is a sort of guide that will allow people to easily join us and select cool research topics to address and write papers about etc. It also allows us to ensure coverage of important core concepts so that we do not end up with rather patchy research with some core areas not addressed. We agreed to structure research activity into three strands of work: Semantics; Methods & Applications and Tools. For example, Hugo’s work will largely fit within the Tools strand.

: Cutting across the three strands of research, we will have Challenges. These are focussed specific problems that bring together research in several areas and allows us to see our progress and also allows us to test out developments. The three main challenges under consideration at the moment are “Mondex”, “Pacemaker” and “Posix”.

: John proposes that the SRA page should evolve by the lead contacts in each stream or challenge soliciting brainstorm lists of open research problems in their area, as well as identifying important base research that should be done in order to provide a suitable platform. For example, in Semantics, John will have “Denotational Semantics of VDM++” as a base topic and “Can we adequately represent LPF in HOL” as an open question. As an example of a challenge, Marcel could propose a specific problem arising out of his doctoral work, such as modelling and analysis of a photocopier controller.

• Action 15/3: Progress the SRA by asking strand and challenge leaders to brainstorm open questions and identify areas of more basic research that shoudl be addressed (John).

Mondex and Pacemaker case studies

Our first challenge is Mondex - an electronic purse system specified and designed via data refinement originally in Z. Several people have expressed interest in tackling Mondex in VDM. This work is being led by Jeremy Bryans at Newcastle. A workshop is scheduled for 2-3 April at Newcastle for the interested people to make concrete progress. Prior to that, a reading group at Newcastle will review the monograph that describes the Mondex study in Z.

The Pacemaker study has now been released and we need to find a champion within the Overture community. It was suggested that CSR Newcastle could again take the lead, with Zoe Andrews contributing, as the application lends itself well to the work that Marcel and Zoe have been doing on stochastic fault modelling. It’s also Zoe’s potential PhD topic, which John would supervise.

• Action 15/4: Produce a concrete proposal for progressing the Pacemaker study. (John, Peter, Marcel)

Any Other Business

John suggested having a discussion of publication status and plans as a regular topic in Overture net meetings.

• Action 15/5: Add publication status and plans as a regular topic in Overture net meetings (Peter).

Next Meeting

4 March 2007 1200 CET