Net Meeting 24

Review of Action List

The actions are all at Overture on SourceForge.

• 13/2 Ongoing.
• 20/1 Closed.
• 20/2 Closed.
• 20/3 Closed.
• 20/5 Closed.
• 23/1 Closed.
• 24/1 Organise SRA meeting at Turku (Tuesday)
• 24/2 Discuss Pacemaker future challenge with McMaster? at FM
• 24/3 Revise and publicise student project lists
• 24/4 Find out about Rodin Tool plug-in standards
• 24/5 Marcel Authorise Sander to edit top page of wiki

VDMTools

Status and development plans for VDMTools version 8.xx

Version 8.1 is now available.

Overture

Status of Adriana’s work on the Overture Test Automation Support

Adriana is starting implementing a combinatorial testing tool for VDM++, based on Tobias Tool. She also wrote a theoretical approach for Mutation Testing in VDM++. A Mutation Testing Tool will not be implemented due to insufficient resources on the Overture.

Status of Carlos’ work on the Overture Connector between VDM++ and JML

Carlos overrun all the major theoretical details that kept him for starting the implementation of the connection between JML and VDM++. He will now start implementing the tool.

Status of Augusto’s work on the Overture Proof Obligation Generator

Augusto is trying to find a way of proving function termination automatically, including nested functions.

Possible new students to take new Overture tasks

Peter will I try to contact José for potential new students who might be interested.

The MONDEX case study

They started this work by concentrating on illustrative proofs of correct refinement. There has been slow progress because it all has to be done by hand. One can see the state of the proof checking on the Wiki page. They still plan to generate a TR including the proofs. However, they have decided to make a main focus the illustration of test-based validation technology using VDMTools (so far the main distinctive selling point of VDM). To that end, Ken has been involved in setting up a testing framework which is now installed in a local SVN repository (along with the emerging TR).

John thinks they can get there in the end but, because this has not been a concentrated effort (because of lack of willingness to commit concentrated resources) it will not tell an encouraging story about VDM. Their lack of proof tools is still a major weakness compared to other formalisms. However, their testing support is impressive. The work has had a beneficial effect in spreading experience in VDM, VDMTools and proof among a wider group here in Newcastle.

The Pacemaker case study

Hugo has so far made the one serious attempt at this study. The models were a good start, but they were mainly developed in order to illustrate a development methodology rather than to make a significant attack on the pacemaker study. Zoe has been looking in detail at some of the models (and indeed is now attempting them in Event-B) and feels that major revisions would be required if they were attempting a serious attack on the study. John’s main concern is that there is no definite specification of what the challenge problem is and, further, how anyone can attempt it without access to domain expertise. For the moment, this remains an example used to illustrate other things. John sees no prospect of that changing unless more people than himself and Zoe commit time and resources, and they get some domain expertise.

• Proposed ACTION: 24/2.

The POSIX

John will update to the BTrees model that has been adopted into the study by Jim Woodcock, based on some old VDM work. José Nuno has a small team working in this area and they are also in contact with Sander.

Publication plans

In preparation:

• Paper path case study (Marcel)
• ACM Computing Surveys paper on industrial applications of FMs (Peter, Juan, John)
• 2nd edition of “Modelling Systems”, Cambridge University Press (John & Peter) by Feb 2008
• VDM++ book (Shin)

In review:

• PhD? thesis (Marcel)

In press:

• FeliCa? paper (Araki, Peter and FeliCa?), to appear at IDay at FM’08
• John Fitzgerald and Cliff B. Jones, The connection between two ways of reasoning about partial functions, Information Processing Letters, to appear 2008.
• Hugo, Peter, John, Incremental Development of a Distributed Real-Time Model of A Cardiac Pacing System using VDM, to appear in Proc. FM 2008
• John, Peter, Shin VDMTools: advances in support for formal modeling in VDM, ACM Software Engineering Notes, to appear 2008
• John, Peter, Marcel, Vienna Development Method, in B. Wah (ed.), Wiley Encyclopedia of Computer Science and Engineering.
• John et al, Animation-based Validation of a Formal Model of Dynamic Virtual Organisations, to appear in P. Boca and J. P. Bowen (eds.) Proc. BCS-FACS Workshop on Formal Methods in Industry.
• Peter and John. Recent industrial Applications of VDM in Japan, to appear in P. Boca and J. P. Bowen (eds.) Proc. BCS-FACS Workshop on Formal Methods in Industry.
• Formal Semantics of a VDM Extension for Distributed Embedded Systems; (Jozef and Marcel) to appear in Festschrift for W P de Roever (LNCS).
• Jozef, A summary of the FM06 and IFM07 paper and enhanced the PVS models, to appear in Festschrift for W P de Roever (LNCS).
• Paper about proof work (Sander), Overture/VDM++ Workshop at FM08

Recently Appeared:

• P. G. Larsen, J. S. Fitzgerald and S. Riddle. Practice-oriented courses in formal methods using VDM++. Formal Aspects of Computing, Springer-Verlag, February 2008 (currently available in online-first) DOI 10.1007/s00165-008-0068-5
• Strategic Research Agenda and Wikipedia
• Peter has worked on Wikipedia entry and it had considerably improved. Feedback from potential readers would be important.

Any other business

Nothing to report.

Next Meeting

20 April 2008, 1300 CET