Welcome to the Overture tool project

Overture is a community-based project developing the next generation of open-source tools to support modelling and analysis in the design of computer-based systems. Overture supports VDM: The Vienna Development Method, a set of modelling techniques with a long and successful history of industrial application and research. Overture is an integrated development environment (IDE) for developing VDM models. The Overture tools are written entirely in Java and build on top of the Eclipse platform. Overture supports the following VDM language dialects:

  • VDM-SL: the VDM Specification Language, ISO/IEC 13817-1:1996, with extensions for modules
  • VDM-PP: Object oriented extension of VDM-SL, also known as VDM++
  • VDM-RT: Extension of VDM++ for specifying real-time and distributed systems 
The current stable version is 1.1.1  (december 2011) which you can download here.

If you want to know what we have to offer, check out this 15 minute video showing our tool at work!


 

Editing

  • Easy editing with color highlighting of keywords
  • Outline of source files for easy navigation

The Eclipse Overture perspective (click on picture for full view)

Checking

  • On-the-fly syntax and type checking
  • Combinatorial testing
  • Proof obligation generation
  • Run-time checking of pre-/ post- conditions, measures and invariants

 The combinatorial testing perspective (click on picture for full view)

Debugging

  • Integrated debugger
  • Advanced breakpoints (conditional/hit count)
  • Stepping
  • Coverage generation and presentation
  • Real-Time time log generation of execution and deployment

Debugging perspective in Overture (click on picture for full view)

Other tool features

  • Latex document generation
  • Coverage Editor
  • Quick Interpreter
  • Proof obligation viewer
  • Import / Export of UML 2.0 class diagrams using XMI
  • Real-time log viewer of deployment and call timing on system architecture