The VDM Strategic Research Agenda

We are developing a SRA for VDM-related research. The objectives of the agenda are:

• To give newcomers to our community a means of quickly finding out what the open questions are, and discovering important new research topics that they can have fun addressing.
• To help us ensure that we are working in a complementary way, covering important research issues, rather than having patchy areas of unfinished and unpublished research.

The SRA is being developed under this Wiki topic. Currently it is structured as follows: There are three key research strands: Semantics, Methods and Applications, and Tooling. Cutting across the strands, we are addressing a series of Challenges which will help us to monitor our progress and provide a concrete focus.

Contribute Topics! Please go ahead and add open questions to the emerging lists under each strand below

Do Research! Our current and planned research activities are discussed on this page. If you would like to contribute to any of them feel free to contact the Contacts for the areas in whcih you are interested.

A Roadmap for VDM-related research

Contacts: (Peter Gorm Larsen, John Fitzgerald, Marcel Verhoef)

Where do we want to be?

In the last ten years or so, our activity has been largely driven towards industry adoption of a lightweight formal methods approach based on executable models and validation through testing. However, if we want to gain long-term benefits form research on VDM we need to ensure that we address the funamental issues in the formalism and tools as well as industrial applications.

Here’s a suggestion. In five years’ time, we would like to be in the following position:

• Tools: Overture should be a recognised leading experimental framework for developing new plug-ins in support of analysing o-o structured formal models, especially for real-time, embedded and distributed systems. VDMTools shall be an even more efficient tool aimed for industrial usage and promising prototype features from Overture are also incorporated.

• Formalisms: VDM should be a leading vehicle for work on grand challenges in computing and interdisciplinary approaches to systems modelling and development

• Industry Application: VDM is being used publicly in large-scale industry projects in Japan and is increasingly being applied industrially both in Europe and in the US.

Some proposed Topics:

• Incorporation of GUI and basic checks already present on the Eclipse platform. Since Overture is developed on top of the Eclipse platform it is essential to make use of the features already supported on that platform. This includes syntax highligthed editors, literate programming support, easy browsing of large models and refactoring support.
• Automation of tests derived from VDM models using different principles.
• Validation overview support in the form of test coverage (both statement and branch coverage), visualisation of executions in different graphical forms and general test automation support in different forms.
• Linking of the VDM interpreters with models written in different other notations. This include the combination of the VICE interpreter with continuous time simulators such as 20Sim or Simulink.
• Mixed-mode discharging of proof obligations (POs). POs can be automatically generated from VDM++ models and Sander Vermolen's project has shown that many can be automatically discharged by a HOL-based prover. Some, of course, can not and for these it might be appropriate to generate tests. This is an instance of the general problem of discharging some lemmas in proofs. In cases where automatic proof of proof obligations is not possible it may be very interesting in gaining a higher level of confidence by generating tests from the POs in question.
• Connection to different standard development environments and notations. This includes code generators and potential combinations with databases. Also issues such as reverse engineering support, generators of GUI applications and connection to graphical notations such as UML2, AADL and SysML^? can be envisaged here.

Formal semantics of VDM++

Contact: John Fitzgerald: also involved: Bernhard Aichernig, Jose Oliveira, Joey Coleman, Peter Gorm Larsen.

There is a denotational semantics (in the ISO Standard), a proof theory (in Bicarregui et al.) and an operational semantics (in VDMTools) for VDM-SL. The work on VDM-SL identified challenges in coping with aspects such as looseness in the proof theory. For VDM++, we still lack a widely accepted semantics that deals with the object-oriented structuring and concurrency present in the language extensions. Topics:

• Denotational style: can we give a denotational semantics to the o-o extensions? How to handle concurrency in this framework.

• Proof theoretic semantics: The focus should be on implementable proof theory, again, taking account of o-o and concurrency aspects.

• Structural Operational Semantics (SOS) offer an opportunity to give an operational semantics in a manner that potentially supports reasoning directly within the semantics, rather than within the proof theory. Further, there is research towards SOS for object-orientation and concurrency. A very interesting topic here is the provision of SOS for the features of VDM-SL and VDM++ that are not cleanly expressed in the traditional denotation/proof theory framework?

The recent work on Real-Time and distribution are likely to bring their own challenges on semantics, and we intend to visit these when Marcel's PhD^? workis completed (Spring 2008).

Connection to JML?

Contacts: Nico Plat, Bernhard Aichernig^?

Semantics amenable to additional tool support

Contact:Peter Gorm Larsen

External and internal tool (in particular related to proof, model checking, connections to SDE's) as described as some of the proposed topics above.

Grand Challenge contribution

Our aim is to contribute to the GC6 Grand Challenge on Dependable Systems Evolution, to demonstrate the role of VDM in system analysis and design, specifically:

• Mondex: use this as a basis for involving more people in the research community. Provide a benchamrking against the state of the art by conducting some sample formal proofs (by hand and using Sander's tools), doing illustrative testing and API-based validation work.

• Pacemaker: use Pacemaker initially as a way of trialling the methodology for Distributed Real-time model development. Consider a full-scale attack onthe Pacemaker study when the study is itself more clearly defined.

• Verifiable (posix) file store: identify a potential contribution area.

-- JohnFitzgerald - 15 Mar 2008