Overture - Open Source Formal Methods Tools

Tool architecture

Principles

The guiding principle in the architecture for the tool 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.

News

26 August 2006
The Third Overture workshop will be held at Newcastle University (27-28 November 2006). Look at the call for participation.

25 August 2006
Papers of the Second Overture workshop that was held on 21 August at FM'06.

11 Sept 2005
The MSc thesis of Jacob Porsborg Nielsen and Jens Kielsgaard Hansen, describing the architecture of the Overture Eclipse plug-in is now available on-line.

Overture © 2004, 2005