Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

Date 2016-02-07 13:00 CET
Participants LF, LDC, MV, NB, PGL, SS, TO, VB, PJ. Minutes by PJ.

Review Status of the Action List

See Net Meeting Actions

Overture Language Board Status

The LB has suggested moving the core meetings from 13:00 CET to 12:00 CET such that the core meeting is immediately followed by the LB NM. There were objections so the new schedule for the core meetings was accepted. In the future the core meetings will therefore start at 12:00 CET. PGL will update the meeting schedule accordingly.

Status of VDMTools Development

Nothing new to report.

Status of the Overture Components


A few bug fixes applied. Build numbers below are VDMJ’s, relevant fixes also applied to 2.3.1-SNAPSHOT

New GUI Support in Overture (part of the TEMPO project)

A new framework for developing UIs for VDM models with DukeScript has been developed (see https://github.com/overturetool/tempo-ui). A very rough proof of concept demo video is available at https://dl.dropboxusercontent.com/u/1587375/uidemo.avi

Two student workers will use this framework to develop a UI for a Traffic Management System model, developed as part of the Tempo project.

Removal of Components from the main build

We have begun removing certain components from the Overture build. These components are not maintained by anyone and provide features that nobody uses. They also slow the build down. They are being migrated into stand-alone repositories in the overturetool GitHub org. So far, we have removed the ProB integration and the old GUI Builder (no relation to TempoUI). More may come (such as the new pretty printer and the test framework).

Overture code generation

Lots of internal fixes and extensibility improvements to the code generation platform. All these improvements are based on feedback from the VDM-to-C code generator and the VDM-RT code generator projects. All the technical details related to this are described at https://github.com/overturetool/overture/issues/491.

In addition to that we have started updating the Isabelle translator to use the newest code generation platform.

Other than that just some bug fixes in the Java code generator.

The VDM-RT code generator that uses Java RMI to represent the distributed communication between the JVMs, has been updated the use the newest features of the code generation platform. Additionally, work has been started on updating the VDM-RT code generator to use the newest version of the VDM++-to-Java code generator. Finally, it is investigated how to integrate the VDM-RT code generator with the Maven build system.

The VDM to C code generator is progressing well, we are working toward generating one of the INTO-CPS case study models, and are very close (roughly a week). This VDM model is itself generated from PLC ladder code, so it is very consistent, and moreover contains a simple but important set of language features to target.

Release Planning

It is expected that there will be a new release of Overture within the near future. PGL’s VDM course will start soon.

Community Development

Overture Traffic

See download stats on the downloads page

Website Issues

The https://www.overturetool.org/ website is built with GitHub Pages Jekyll. GitHub is updating Jekyll and the current rendering engine is being discontinued (May 1) so we need to migrate. The new version looks mostly fine but we need someone to test it before start using it.

The old Overture Wiki

The old wiki (wiki.overturetool.org) is still on-line. PGL will take an action to follow up and talk to IT about taking it off-line.

Publications Status and Plans

See Planned Publications.

Any Other Business

TO made ViennaTalk videos - see https://www.youtube.com/watch?v=ZIR3fFPeTz0 and https://www.youtube.com/watch?v=anZoWeA5vd0 . Feedback on these videos are very welcome.

There’s now a “Related tools” section on the overturetool website: https://www.overturetool.org/community/related-tools.html