The VDM Research Agenda

The research agenda is mid-revision. Sorry for the state of this page at the moment! Contact: John Fitzgerald

The purpose of this agenda is to identify and prioritise open research questions and to ensure that we are working in a complementary way rather than having patchy areas of unfinished and unpublished research.

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 on this page, feel free to get in touch with the listed Contact for the area that interests you.

Our aim is to ensure that by 2015:

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

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

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

Currently the SRA is structured as three key research strands:

• Semantics: the aim of semantics research is to develop a formal semantics, broadly accepted by the community, that covers the object-oriented structuring and concurrency present in the language extensions. The semantics strand is described on the Semantics Page.
• Methods and Applications: the aim of this strand is to
• Tooling: the aim of this strand is to

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.

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 - 26 Sep 2010