Net Meeting 23
||20 January 2008, 1300 CET
||Peter Gorm Larsen, JohnFitzgerald, Carlos Vilhena, Adriana Santos, Hugo Macedo, Shin Sahara, MarcelVerhoef, Augusto Ribeiro and SanderVermolen
Review of Action List
The actions are all at Overture on SourceForge.
- 13/2 Ongoing.
- 15/2 Closed. Thomas has updated the Overture site with his work now.
- 16/1 Closed.
- 20/1 Ongoing.
- 20/2 Closed.
- 20/3 Ongoing.
- 20/4 Closed.
- 20/5 Ongoing.
- 23/1 New: Peter Gorm Larsen to ensure that Posix progress is on NM
- Status and development plans for VDMTools version 8.xx
- Released version 8.0.1b-080115. Struggling with automotive companies
- How to write requirement specification (not only by using VDM,
especially for plant models);
- How to write detailed design specification (by VDM).
Development plans: High priority:
- Test case generator from proof obligation (model based test);
- Eclipse-nize of VDMTools;
- XMI interface;
- Using AST by user.
Priority under consideration:
- VICE improvement;
- VDM with SAT/SMT solver.
- “Japanizing” error messages;
- Alternative tool of CORBA interface.
- Bug reporting for VDMTools bugs
- There are no English reported bugs.
- Status of Thomas’ work on the Overture type checker
- It has now been uploaded but it is only for a subset of VDM++ and it
has not yet been code generated.
- Status of Hugo’s work on the Overture interpreter
- With the high priority of the VDMTools development to the eclipse
platform there will be an opportunity to improve Hugo’s work.
- Status of Sander’s work on the Overture proof support
- Improving the proof support.
- The MONDEX case study
- Nothing to report.
- The Pacemaker case study
- Nothing to report.
- Introduction to new Overture subjects (Adriana, Carlos and Augusto)
- Concerning Carlos’s thesis, he is writing about the possible
limitations of a connection between VDM++ and JML, and comparing the
semantics of both languages. Right now, he is starting the practical
side of his work together with his writing, that will start with
some important decisions evolving the JML parser.
: Adriana is working on test automation support. She has been working
with Tobias, which is a combinatorial testing tool. She made 2
examples in order to use it: the Triangle Problem and the Towers of
Hanoi. She also made the test coverage using the vdmtools. At the
moment, test sequencing seems to be one good choice to implement in
the Overture. The VDMTesK? tool is in stand-by. We are waiting to
hear some news from the developers. They will try to find out why
the tool isn’t working properly. She has been also reading about
mutation testing and will probably have access to another tool which
applies this strategy. Besides all this, she is also writing her
: Augusto’s thesis started this week and the subject is proof
obligation generation for Overture. His work will focus on trying to
extend the current POG to generate obligations for recursive
- Paper path case study (Marcel)
- 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 Feb 2008
- VDM++ book (Shin)
- Wiley Encyclopedia of Computer Science & Engineering entry on “VDM”
(John, Peter, Marcel) - revised following review comments.
- “The Connection between Two Ways of Reasoning about Partial
Functions” (John and Cliff), submitted to Information Processing
- PhD? thesis (Marcel)
- Pacemaker modelling & validation FM08 (Hugo, Peter, John)
- Paper about proof work FM08 (Sander)
- “Learning by Doing” (John, Peter, Steve Riddle), accepted by FACJ
special issue on education
- VDM in Japan (Peter, John), BCS FACS workshop
- Dynamic Coalitions (John, Jeremy et al.) BCS FACS workshop
- Traces Paper (John, Peter, Simon, Marcel), accepted by HASE07
- New Wikipedia entry on “VDM”, replacing current separate entries on
VDM and VDM-SL. (John)
- Formal models of access control in XACML (Jeremy,John) at ICFEM 2007
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 advertise all about ICTAC (http://www.ictac.net/ictac08).
Submissions by 11 April and there will be a special track on tools. The
chairs will be John and Anne Haxthausen and they have completely
revamped he programme committee so the conference will be more applied.
Sander said that a PhD? student at Delft University is working on
generating language plugins for Eclipse based in their grammars
(specifically dsls) to support highlighting, syntax checking code
2 March 2008, 1300 CET