Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

Net Meeting 27

   
Date 20 July 2008, 1300 CET
Participants Peter Gorm Larsen, JohnFitzgerald, Carlos Vilhena, Adriana Santos, Shin Sahara, MarcelVerhoef, Augusto Ribeiro, Kenneth Lausdahl, Miguel Ferreira and Nick Battle.

Review of Action List

The actions are all at Overture on SourceForge.

VDMTools

Status of the VDMTools

:* Fixed bugs: No.239, 252

:* Not yet fixed bugs: No.248, 249, 252, 253, 254, 256

Status of the VDMTools project
CSK, SRA and Prof Araki proposed a research project to METI (Ministry of Economy, Trade and Industry):
  • A guideline for using VDM in industry
  • A guideline for using Haskell in industry
  • A converter which converts functional VDM-SL specifications to Haskell.

Brother companies, CSK Systems Chubu (in Nagoya) and CSK Systems Nishi-Nihon (in Osaka) started VDMTools sales activities: CSK Systems Nishi-Nihon got the research project of METI with AIST(Advance Industrial Science and Technology?)

:* The project uses Agda and VDM

Sales of VDMTools
Our sales found many candidates of VDM user, but they are the candidate yet

Education

:* Prof. Hagiya in Tokyo University will use my VDM++ seminar materials in computer language class.

:* A small company (TAO bears LLC) wants to use my VDM++ seminar materials in their formal method seminar course.

Overture

Overture Parser Update

Nothing to report.

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

Adriana finished the first version of the combinatorial testing tool. It is now possible to automatically generate test cases from traces. However, there are some limitations which should be take into consideration as future work. In order to finish her’s work, she had to implement the pretty printer for VDM++, together with Carlos, who also needed it for his work. They did not cover all the 277 classes, but a very larger number was covered and already successfully tested with our specifications. However, further testing should be done in order to guaranty its correctness. There are also some things to improve, e.g. indentation.

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

After delivering the thesis and the specification, he made some improvements on the mapper. Besides, he built a java application to make it usable.

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

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

A new MSc student will be working part-time over the next 12 months. Sarah Clarke will work on a demonstration of GUI-based validation of the executable Mondex models. In this she will be helped on the interface design by David Greathead, the psychologist who worked with us on the dynamic coalitions stuff. We have allocated two remaining Mondex days at Newcastle: 30 July and 1 August, when we hope to complete the proof work. Sarah has added a topic to the wiki (linked from the Mondex topic) to serve as a reporting base. Thereafter the target is to prepare a paper for a planned special issue of FACJ with completion 4Q08 as I previously reported.

The Pacemaker case study

John have agreed to become the UK owner of the Pacemaker problem for GC6 (the initiative on challenge problems for software verification). Several initiatives to fund full-time work on the pacemaker and other GC6 problems are underway and I will not bore you all with the details. One that he will explore is the possibility of setting up an EU network on formal techniques and certification of critical systems, to mirror the North American group. He will be working on the Pacemaker models in August and will give a presentation on the state of the Pacemaker study on 15 September at the ASM conference in London. 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

Before the last NM Miguel was translating the FS_OpenFileDir operation to Alloy so that it could be model checked. Since then he have completed the verification of the FS_OpenFileDir and started to use the VDM Unit Test framework explained in the VDMBook. Unit testing as been of great use making it easier to layout the test suites, but because it is a very simple architecture it doesn’t show the assert where the test failed. From the verification of the FS_OpenFileDir (opens or creates a file or a directory) operation i found 2 bugs by model checking:

All POs generated by the VDMTools where model checked with success in Alloy. As for proof I used the Automatic Proof Support system to discharge them in HOL:

One of the POs that was taking tow long is about the FileStore? invariant preservation (the others are related to extra VDM constructs inserted fo allow the translation). For this PO I tried to use HOL to calculate a precondition that would make the operation sustain the FileStore? invariant. I had to follow HOL’s proof step by step in order to understand the sub goals that were being generated (so it was harder than doing it my self!!). I eventually reached a predicate for the pre condition that would hold the invariant, but my intuition was that this new predicate was just equivalent to the initial predicate I had written. So he asked HOL to prove that the predicates are in fact equivalents, which it did. There are two new operations being written/verified which are FS_SetFileOffset and FS_WriteFile. After these operation have been verified he will start to prepare the refinement work, trying to represent the File System Layer data structures in Data Object Layer data structures.

Overture Workshop

José Nuno suggested Braga, in Portugal.

Publication plans

In preparation:

In review:

In press:

Recently Appeared:

Any other business

An Overture Summer School was suggested and it will be discussed in the next meeting.

Concerning eclipse integration I can say that I have a new student (Christian) to do a small project (150 hours) this authum on that + if it goes well continue with that as his MSc thesis from January. Phase one will include integration of newest parser in the eclipse editor and invocation of VDMTools as well.

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. They have put the latest information about the rCOS tool on our webpage, the first version is released. The tool , and eclipse update can be used to download the latest version.

Nick Battle has been developing a java implementation of a VDM-SL parser, type checker and interpreter.

Next Meeting

7 September 2008, 1300 CET