Net Meeting 20
||26 August 2007, 1300 CET
||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
- 15/3 Closed.
- 15/4 Closed.
- 16/1 Ongoing.
- 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
- :*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
- 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.
- 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.
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
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.
- 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
- Wiley Encyclopedia of Computer Science & Engineering entry on “VDM”
(John, Peter, Marcel)
- “Learning by Doing” (John, Peter), submitted to FACJ special issue
- “The Connection between Two Ways of Reasoning about Partial
Functions” (John and Cliff), submitted to Information Processing
- Traces Paper (John, Peter, Simon, Marcel), accepted by HASE07
- Formal models of access control in XACML (Jeremy,John) accepted by
- 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).
- MSc Thesis (Sander)
- IFM Paper (Marcel et al.)
- DSN Fast Abstracts (Zoe, Marcel, John, Jeremy)
- 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
: 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
: GC6 is planning a series of Grand Challenge workshops. Current
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
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
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.
14 October 2007, 1300 CET