Net Meeting 40
||3 January 2010, 1300 CET
||Peter Gorm Larsen, John Fitzgerald, Shin Sahara, Marcel Vaerhof, Nick Battle, Carlos Vilhena, Sako Hiroshi, Augusto Ribeiro and Kenneth Lausdahl.
Review of Action List
The actions are all at Overture on SourceForge.
- 38/2: still open. As indicated at the last NM, Marcel and John will
address this later in January when they are together in Twente in
Shin sent out the usual VDMTools report (see overture-core list).
Status for each of the Overture components at sourceforge
Traces: We are still working on the paper and have made some minor bug
- The new feature of VDM-10 have been made available through a
property tab on a project.
- New launch tab has been made. Now there is no need to select a file
name anymore, just the class/ module and operation/function. Here a
number of bugs has been fixed. E.g. starting the debugger with a
string argument for an operation.
- The debug launcher now takes a argument for memory in the
overture.ini into account when starting so we can increase the
memory allowed for the debug virtual machine.
- A coverage option has been added to the launch configuration and
will soon be available when running a VDM model. VDMJ already
includes all the information.
- A small test feature has been added to the Overture debug helper
plug-in to enable generation of latex – pdf document of a model.
- PO Viewer: Here the GUI has been upgraded so it keeps the same
numbering even when the filter option is enabled. Additional bug
fixes has also been made.
Overture Language Board
Only Peter and Nick have stated their wish to be re-elected. Nick will
work on re-establishing the LB for the next NM. Action 40/1.
Nick suggested that release policy should be managed via the LB via
“issues” - except for the third-digit builds. There is always an
outstanding release “issue”, and developers working to implement it.
Action (40/2) on Peter to coordinate a release plan that has the
support of core members and DESTECS. He can start this during the
DESTECS Kick-off but it will have to be discussed with core before being
Planned (note the lead author and approximate date):
- DESTECS paper on static correctness conditions for co-simulation
(John, June 2010)
- DESTECS paper on co-simulation incl. tool support (Peter, end 2010,
aiming for FM’11)
- DESTECS paper on case studies (Marcel, aiming for an I-Day in 2010
- DESTECS paper on fault modelling in VDM and in co-sim framework
- Paper path case study (Marcel & Jozef, target end January 2010) for
Journal of Systems and Software
- Japanese Translation of VDM++ Book (Sako)
- POs for Recursive Functions (Augusto, Peter)
- CT (Kenneth, Peter, Nick)
- DESTECS project introduction (Peter, Jan Broenink, Marcel, et al.,
due January 2010)
- Overture Introductory paper aimed at ACM SE Notes (Peter, Nick,
Miguel, John, Kenneth, Marcel) – due January 2010.
- New proof paper (Sander, Peter, Jozef) accepted to SAC
- Formal Semantics of a VDM Extension for Distributed Embedded Systems
(Jozef and Marcel) in Festschrift for W P de Roever (LNCS 5930) –
due January 2010.
EVERYONE please remember to update the publications list on
EVERYONE please remember to acknowledge DESTECS in any relevant
Any Other Business
- Three Overture tool introductions have been prepared for the 3
dialects, each as a replacement Chapter 3. We’ll get reviews of the
draft chapters from colleagues.
- A guide to Overture for potential adopters: Actions 40/3 and 40/4 -
Peter and Nick to review older VDM marketing materials.
6 February 2010, 1500 CET