Net Meeting 26

Date estimated!

Review of Action List

The actions are all at Overture on SourceForge.

• 24/1 Closed.
• 24/2 Closed.
• 24/4 Find out about Rodin Tool plug-in standards.
• 25/1 Produce plan with Jeremy for final stages of Mondex
• 26/1 MARCEL: Get NM participants to sign up to SF

New items

Cool new Eclipse features discovered recently

News about the rCOS tool

VDMTools

Status and development plans for VDMTools version 8.xx

Nothing to report.

Overture

Overture Parser Update

Nothing to report.

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

Adriana made the expanded version of the traces written by the user.

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

Carlos got the JML parser interacting with his mapper. He will continue mapping from VDM to JML in VDM++.

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

Augusto finished the implementation of the POG, apart from some minor things involving classes that are not working properly.

New students (Kenneth and Hans Christian)

Kenneth and Hans Christian will development a tool similar with Rose link from VDMTools. They will extend the overture project with an eclipse plugin (EMF) for going back and forth between VDM and UML. Additionally they will take a look at the test trace file and see if it is possible to pars this file into a UML sequence diagram.

The MONDEX case study

Jeremy and John have discussed a substantial paper on Mondex for FACJ with Jim Woodcock, who is planning a special issue on Mondex follow-up. The one thing John would like to show that was not done so far is a GUI for domain expert validation. John has a student who wants to work in this area but she is going to be part time and will take long. He is considering whether he can divert PhD? student resource on this at Newcastle.

The Pacemaker case study

Pacemaker FAQ is in the wiki at http://www.cas.mcmaster.ca/wiki/index.php/Pacemaker_FAQ The head of wiki is: http://www.cas.mcmaster.ca/wiki/index.php/Pacemaker John will give an invited talk on the pacemaker work as part of a GC day immediately preceding the ABZ conference in London in September. He will work further on Pacemaker before then.

The POSIX

Improvements were made in proving the proof obligations automatically in HOL. A vote of thanks to Hugo and Miguel is made for speaking at the GC workshop - it got the community a lot of good publicity and improved recognition in the GC community. They liked the way the community is using the challenges to explore and benchmark different aspects of the VDM technology. Miguel is preparing a page for the VDMPortal compiling all the material they have so far.

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) - goes to CUP for review this week

In review:

• PhD? thesis (Marcel)
• Tools for Policy Design in Virtual Organisations: A Proof-of-Concept Study (Jeremy & John to submit to ICFEM’08)

In press:

• John, Peter, Marcel, Vienna Development Method, in B. Wah (ed.), Wiley Encyclopedia of Computer Science and Engineering.
• Jozef and Marcel: Formal Semantics of a VDM Extension for Distributed Embedded Systems; 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).
• VDM++ book (Shin Sahara)

Recently Appeared:

• Modelling and Analysis in VDM: Proceedings of the Fourth VDM/Overture Workshop, Fitzgerald J.S., Larsen P.G., Sahara S. (eds.), Technical Report CS-TR-1099, School of Computing Science, Newcastle University, May 2008. http://www.cs.ncl.ac.uk/publications/trs/papers/1099.pdf Includes several papers previously listed as “in preparation”.
• Final version of J.S. Fitzgerald, C.B. Jones, The Connection between Two Ways of Reasoning about Partial Functions, Information Processing Letters (2008), 107(3-4), pp. 128-132, 2008 (Ncl: CS-TR-1044)
• T. Kurita, M. Chiba and Y.Nakatsugawa, “Application of a Formal Specification Language in the Development of the “Mobile FeliCa?” IC Chip Firmware for Embedding in Mobile Phone” in J. Cuellar, T. Maibaum and K. Sere eds., “FM 2008: Formal Methods”, LNCS 5014, pp 425-429.
• Hugo, Peter, John, Incremental Development of a Distributed Real-Time Model of A Cardiac Pacing System using VDM, in J. Cuellar, T. Maibaum and K. Sere eds., “FM 2008: Formal Methods”, LNCS 5014, pp 181-197.
• John et al., Animation-based Validation of a Formal Model of Dynamic Virtual Organisations, in P. Boca, J. P. Bowen and P. G. Larsen (eds.) Proc. BCS-FACS Workshop on Formal Methods in Industry. http://www.bcs.org/upload/pdf/ewic_fm07_paper3.pdf
• Peter and John. Recent Industrial Applications of VDM in Japan, to appear in P. Boca, J. P. Bowen and P. G. Larsen (eds.) Proc. BCS-FACS Workshop on Formal Methods in Industry. http://www.bcs.org/upload/pdf/ewic_fm07_paper8.pdf

Any other business

An Overture Summer School was suggested and it will be discussed in the next meeting. The members of the Overture community should take an action to investigate the rCOS plug-ins. A description of the rCos tool is available on http://rcos.iist.unu.edu/tool.

Next Meeting

20 July 2008, 1300 CET