The VDM Strategic Research Agenda

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

• To identify open research questions.
• To help ensure that we are working in a complementary way rather than having patchy areas of unfinished and unpublished research.

Currently the SRA is structured as three key research strands: Semantics, Methods and Applications, and Tooling. Cutting across the strands, we are addressing a series of specific 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! If you would like to contribute to any of the topics listed ont his page, feel free to get in touch with the listed Contact for the area that interests you.

Where do we want to be?

Our aim is to ensure that by 2015:

• Formalisms: VDM should be a leading vehicle for work on grand challenges in computing and interdisciplinary approaches to modelling and developing a range of systems including real-time, embedded and distributed systems.

• 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 should be an even more efficient tool aimed for industrial usage and promising prototype features from Overture are also incorporated.

• Industry Application: VDM is being used publicly in large-scale industry projects in Japan and is on trend of increasing application in Europe and in the US.

Key Research Themes

Formal Semantics

Contact: John Fitzgerald

State of the Art: 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. For VDM-RT, a starting point for semantics exists in the work of Verhoef and Hooman. The DESTECS project will support the development of a basic semantics of co-simulation.

A complete semantic definition for VDM++ and VDM-RT is important for the development of a consistent set of tools, so we propose an effort to produce a semantic definition of a unified VDM language which we will refer to as VDM-10. The Overture Language Board is coordinating efforts to develop a working language definition with formal semantics. Starting points for a VDM-10 Language Definition are discussed in the VDM-10 Semantics Topic.

Methods and Applications

State of the Art:

Open Topics:

• Methods for the development of embedded systems.

Tool Support

State of the Art:

Open Topics:

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

Challenge Problems

The purpose of the challenge problems is to provide a benchmark for VDM technology against our goals in demanding application areas and, to a limited extent, provide a basis for comparison with other formalisms and tool sets.

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

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

• 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.

Some Project 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 highlighted editors, literate programming support, easy browsing of large models and re-factoring 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.

-- JohnFitzgerald - 23 May 2010