Net Meeting 21
||14 October 2007, 1300 CET
||Peter Gorm Larsen, Hugo Macedo, Shin Sahara, Emma Nicholls,Adriana Santos and Carlos Vilhena
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
- 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.
- 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.
- 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
- 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
- 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
- Wiley Encyclopedia of Computer Science & Engineering entry on “VDM”
(John, Peter, Marcel) - review comments have been promised
- “The Connection between Two Ways of Reasoning about Partial
Functions” (John and Cliff), submitted to Information Processing
- MSc Thesis (Hugo)
- 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
- Workshop submission on visualizing models of access control
- “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.
18 November 2007, 1300 CET