Main WebOverture - 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
January 2010: A guided tour introducing Overture to new VDM++ users and A guided tour introducing Overture to new VDM-SL users is now available as a replacement chapter from the VDM++ book and the VDM-SL book respectively. A similar tutorial is available for VDM-RT (formerly called VICE) users. November 2009: Materials from the 7th Overture Workshop held at FM 2009 in Eindhoven, the Netherlands, are now on-line. The proceedings of the workshop are available as a technical report from Newcastle University. May 2009: Materials from the 6th Overture workshop, held on 7-8 May 2009 at Newcastle University, are now on-line . The workshop focussed on encouraging tools development. February 2009: The call for papers for the Overture workshop to be held at the FM'09 conference is now on-line. November 2008: A Frequently Asked Questions on the use of our Sourceforge based development environment has been added. November 2008: The 5th Overture workshop was held on 8-9 November 2008 in Braga, Portugal. This was a real "work shop" at which participants exercised different aspects of the development of Overture components on 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++
Overture Mission
Overture's mission is twofold:- to provide an industrial-strength tool that supports the use of precise abstract models in any VDM dialect for software development, and
- to foster an environment that allows researchers and other interested parties to experiment with modifications and extensions to the tool and the different VDM dialects.
The Overture Community
The Overture tools are being developed by volunteers, research scientists and students. You can find an overview of us at WhoIsWho. 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.The Overture Community Process
Contributions to Overture, the language definitions and pther aspects, are handled through the Overture Community Process.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
Download the Overture IDE and standalone modules from out Source Forge page:
Notes, Tech Reports and Publications
See our reports page for copies of technical papers and materials related to Overture. -- PeterGormLarsen - 03 Jan 2010
Log In
Main Web
Users
Groups
Index
Search
Changes
Notifications
Statistics
Preferences
Main |
|
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors. Ideas, requests, problems regarding Overture? Send feedback