Overture - Open-source Tools for Formal Modelling

This site provides information on the Overture Initiative: a community-based project to develop next generation tools supporting formal modelling and analysis in the design of computer-based systems. Overture builds on a long history of research and industrial application based on VDM: The Vienna Development Method. This is one of a group of Wiki-based sites on VDM, tools, applications and education.

Latest News

August 2008: The 5th Overture workshop will be held on November 8th and 9th 2008 in Braga, Portugal and this will be a real "work shop" where the attendees will exercise different aspects of development of Overture components on top of the Eclipse platform.

May 2008: The 4th Overture workshop Proceedings are online.

May 2008: major new release of the Overture Parser, with position information in the parse tree. Also experimental language extensions to express test traces.

February 2008: The 4th Overture workshop in May 2008 in connection to the FM'08 conference including the final programme.

July/August 2007: Web pages with results of recent student projects are now available (later to be made available at SourceForge):

• TypeChecker for VDM++
• InterpreterDebugger for VDM++
• AutomaticProof support for VDM++

15 January 2007: The Third Overture Workshop was held at Newcastle University, UK, on 27 and 28 November 2006. The topic was semantics and tools, and the aim is to set a research agenda on foundations, semantics and tool support for VDM and Overture. The main outcome was the establishment of three research groups in semantics, tools, and methods and applications.

15 January 2007: Papers from all Three Overture Workshops are now available on the Wiki.

>> All News Stories <<

Overture Mission

Overture's mission is twofold:

• to provide an industrial-strength tool that supports the use of precise abstract models in software development, and
• to foster an environment that allows researchers and other interested parties to experiment with modifications and extensions to the tool.

The Overture Community

The Overture tools are being developed by volunteers, research scientists and students. Anyone interested (from both industry and academia) is welcome to join the project as an active member. You might be interested in contributing directly to tools building (via our Overture open source project at Sourceforge, or you may be interested in developing the formal foundations of VDM++ and Overture.

If you are a student (BSc, MSc, PhD), we can provide cool practical and theoretical projects.

The Overture community meets together at occasional Workshops and monthly via on-line Net meetings using Messenger. To get details of our meetings, please join the Overture mailing list by contacting.

Overture Technology

All the Java source code and public documents will be maintained through SourgeForge.

Principles

The guiding principle in the Overture tool architecture is that it should be based upon a collection of loosely coupled, highly cohesive components. A component-based architecture is attractive both from the point of view of ease of developing, testing and maintainance, but also with respect to the requirement for distributed development in an open-source project.

Extension points Eclipse defines the notion of an extension point as a way that a plug-in can be extended by other plug-ins. This allows component-wise development of tools, which in turn leads to easier development and maintainance. We envisage a small kernel component which defines extension points. Functionality can be added to the core by creating plug-ins for these extension points. Note that plug-ins can also define their own extension points.

Kernel The kernel should consist of the XML parser, an abstract syntax class hierarchy supporting visitors and management functionality. Eclipse has a notion of builders; a builder is a plug-in which is automatically notified when a source file is modified. This allows for efficient plug-ins, since a builder can either reread the whole parse tree, or it can just fetch the changes made since the last notification. We imagine that a large part of the management functionality will be related to handling builders.

Plug-ins We envisage that all components beyond those in the kernel will be written as plug-ins. Thus there will be a type checker plug-in, an interpreter plug-in and so on. It is possible for a plug-in to define dependencies to other plug-ins; the Eclipse platform checks these dependencies at start up and only enables a plugin if all its dependent plug-ins are available.

Downloads

Overture Eclipse plug-ins The Overture software can be downloaded. The software is organised as a Maven project and it is divided into a number of components organised as SubProjects.

You need to have a version of Eclipse (preferably the SDK edition of version 3.4.1 or later) already installed on your system. Using Eclipse, it is possible to download the tool set using the Update Manager. In order to download the software, proceed as follows:

1. Go to Help > Software Updates > Find and Install;
2. Select "Search for new features to install" and press "Next";
3. Press "New Remote Site";
4. Enter "Overture" as the name and "http://www.overturetool.org/updatesite" as URL and press "OK";
5. Check the box in front of "Overture" and uncheck "Ignore features ...", then press "Next";
6. Check the box in front of "Overture Feature" and press "Next";
7. From here on you can follow the instructions provided by the Update Manager.

XML Schema definition for Overture You can download the XML Schema definition for Overture.

Notes, Tech Reports and Publications

See our reports page for copies of technical papers and materials related to Overture.

-- PeterGormLarsen - 15 Nov 2008