Overture Projects for Students

Background

Overture is an open-source project aimed at developing a comprehensive tool set for VDM++ on the Eclipse platform. It is an international project run by a core group of people ranging from Japan to different places in Europe. We meet once a month electronically using MSN. The project should be based on an existing kernel able

• to construct an abstract syntax tree from a VDM++ specification,
• to convert this tree to XML,
• to reconstruct the tree from XML, and
• to provide an Eclipse based editor for VDM++ specifications.

The kernel has been designed so that different tools/plugins can operate directly on the abstract syntax tree via visitor patterns. The original kernel was developed by two students from the Technical University of Denmark as their MSc thesis project. It is the intention that future plugins can be developed independently. The current parser for Overture can be found here. On this page we describe projects that students can carry out either at Bachelor, Masters or PhD levels (the indications provided below are advisory). You should have an interest in software development and software tool building. For most of the projects it is an advantage to have competent knowledge of compiler construction. Your report or thesis needs to be written in English in order to enable all of the involved stakeholders to understand the work performed. If you have an interest in any of the projects listed below feel free to contact us for a dialogue extending the contents of the particular project you have an interest in.

Projects

Development of an Overture/VDM++ Static Semantics checker (Master's level)

This project should be carried out at the Masters level and it aims at developing a static semantics checker on top of the existing Overture kernel platform. A VDM-SL specification of a similar static semantics checker used inside VDMTools is also available as an important starting point. This project shall explore possibilities for extending the Overture kernel with an extensible static semantics checker with a good performance. From a theoretical point of view the static semantics can also be formally related to the static semantics from the ISO VDM-SL standard for the common constructs. If possible the static semantics checker shall also be able to enrich the abstract syntax trees with additional type information that subsequently can be used by different code generator extensions. This project will be a follow-up project extending the development done by ThomasChristensen in his MSc thesis project from Aarhus University in Denmark.

Development of an Overture/VDM++ Interpreter (Master's level)

This project should be carried out at the Masters level and it aims at developing a dynamic semantics interpreter on top of the existing Overture kernel platform. A VDM-SL specification of a similar dynamic semantics stack-machine-based interpreter used inside VDMTools is also available as an important starting point. This project shall explore possibilities for extending the Overture kernel with an extensible dynamic semantics interpreter with a good performance. From a theoretical point of view the dynamic semantics can also be formally related to the dynamic semantics from the ISO VDM-SL standard for the common constructs. Initial work on this project has been made by Hugo Macedo from Minho University in Portugal when he was an exchange student at the Engineering Colleage of Aarhus in Denmark. This project will take his initial work as a starting point.

Develkoment of an Overture/VDM++ Proof Obligation Generator (Master's level)

This project should be carried out at the Masters level and it will develop tool support to enable automatic generation of proof obligations for VDM++ models. This will be based on the MSc thesis of Bernhard Aichernig from TU Graz in Austria. A functionality similar to that is already evailable in VDMTools. However, more exploration will have to be made for the statements part of the language. A part of this project is currently being undertaken by Augusto Ribeiro from Minho University as an exchange student at the Engineering Colleage of Aarhus with focus on proof obligations and the corresponding proofs for definitions that have recursion.

Development of an Overture/VDM++ Automatic Discharging of Proof Obligations (PhD or Master's level)

This project should be carried out at the PhD or Masters level and it will develop tool support to enable proof obligations to be discharged automatically by means of a theorem prover or model checker. This project will use inspiration from the European ESPRIT project PROSPER where this functionality was added to the VDM-SL version of VDMTools. Since a proof obligation generator does not yet exist for Overture this will be generated from VDMTools. This project will be a follow up of the work carried out by by Sander Vermolen who did his MSc thesis work from Radboud University at Nijmegen in The Netherlands as an exchange student at the Engineering Colleage of Aarhus in Denmark. The results of his work is impressive but much more work is needed on top of this.

Development of an Overture/VDM++ Interactive Proof Support (PhD or Master's level)

This project should be carried out at the PhD or Masters level and it should enable users to carry out proofs interactively. This should naturally only be used for proofs that cammot already be discharged automatically. A GUI version of similar functionality was developed for a subset of VDM-SL in the European ESPRIT project but that is no longer available anywhere, such it can only be used as inspiration. However, this project is rather large so it is possible to break it into a series of MSc projects building on top of each other.

Development of Model-checking support for a subset of VDM++ (PhD or Master's level)

This project should enable users to model check parts of a VDM++ model that can be analysed this way. This could be carried out by transforming a subset of VDM++ to an existing model checker such as SAL. However the project can investigate pros and cons for the alternative solutions.

Development of Overture/VDM++ Code Generators (Master's Level)

This project should be carried out at the Masters level and it aims at developing a code generator for automatically generating executable C++, Java or C# code on top of the existing Overture kernel platform. It is anticipated that this project will need input about type information inferred from the static semantics checker so this project cannot be completed prior to the completion of the static semantics checker. However, this project is rather large so it is possible to break it into a series of MSc projects building on top of each other.

Development of Overture/VDM++ Test automation support (Master's level)

This project should be carried out at the Masters level and it should provide functionality to automate test support for VDM++ models. There are different ways in which this can be done based on different results published for similar technologies in the past. This project is currently being undertaken by Adriana Sucena from Minho University on an exchange to the Engineering College of Aarhus until summer 2008.

Development of an API interface to Overture (Master's level)

This project could for example establish a CORBA-based API to Overture such that Eclipse with Overture on top of it can be driven from an external application via the API. This requires getting deply into CORBA as well as the inner workings of Eclipse. It is possible to get inspiration from the API for VDMTools but it does not need to be made in the same way.

Development of Overture/VDM++ Refactoring functionality (Bachelor's or Master's level)

This project could be carried out either at the BSc or the MSc level depending upon the depth and the level of support for refactoring of VDM++ models made on top of the Overture Eclipse platform. In the MSc thesis work from the two students from the Technical University of Denmark the direction for such a refactoring plug-in is indicated. Refactoring is a rather new technology used for changing models during development when improved understanding become present and better ways of describing a solution become clear. It is possible to assist the users with performing such refactoring and this project aims to take the general theory for refactoring and then apply it to VDM++ on top of the Overture Eclipse kernel.

Incorporating More Eclipse Features for Overture (Bachelor's or Master's level)

This project could be carried out either at the BSc or the MSc level depending upon the depth and ambition level for using the more advanced Eclipse features in Overture. The features that could be considered here are builders, monitors, jobs and incremental parsing. Builders are make-like facilities taking dependencies between files into account. Monitors and jobs can be used to enable the user to continue working while threads in the background carry out different kinds of analysis of the model being developed by the user.

Coupling Overture to MDA and UML/SysML (Bachelor's or Master's level)

A translation enabling round trip engineering from Overture abstract syntax to Eclipse Modelling Framework (EMF) with the Meta Object Facility (MOF) shall be developed. From a UML/SysML perspective one will probably map to something like XMI. Having this translation shall enable the move of examples using older versions of Overture models to a new syntax in case of syntax changes by defining appropriate translations at the MOF level. This project should also provide a proof of concept of this being feasible such that language extensions/changes becomes easy to conduct for other students who wish to experiment with that. Finally this project should explore to what extend it would be possible to make round trip engineering to Eclipse-based UML tools in the same way as VDMTools currently is able to couple up together with Rational Rose. This exploration should include a clarification whether any new features in UML2.0 with advantage can be exploited as well.

Automatic generation of GUI's for VDM++ models (Master's level)

This project should enable the automatic generation of prototype GUIs for VDM++ models. It must be clarified how a model shall be annotated to identify the parts that a GUI should be generated for. However, this project should also include a prototype proof-of-concept implementation of the feature on top of the Eclipse platform as a part of Overture and a small case where it has been used.

Connecting between VDM++ and JML (Master's level)

This project aims to explore the possibilities for automatic translation from a subset of VDM++ to the Java Modelling Language (JML) enabling VDM++ to act as a front-end for contract-based programming. this project both needs to contain a theoretical exploration of the subset where this is possible and also a prototype proof-of-concept implementation of the feature on top of the Eclipse platform as a part of Overture. This project is currently being undertaken by Carlos Vilhena from Minho University on an exchange to the Engineering College of Aarhus until summer 2008.

Reverse Engineering Support

This project aims at exploring the possibilities of supporting reverse engineering from a subset of Java to VDM++ on top of the Overture platform. This project will both require a theoretical exploration of the limitations as well as a prototype implementation demostration a proof of concept.

Slicing support for VDM++

This project aims at examining how slicing techniques can be applied to VDM++ and how prototype proof-of-concept tool support on top of the Overture platform can be developed.

Deadlock analysis for VDM++

This project is meant to explore different techniques and approached to detect deadlock in concurrent VDM++ models. Both static and dynamic analysis techniques are to be explored and proof of concept prototypes can be implemented on top of the Overture platform. Here the communication of the detected potential deadlocks to the VDM++ user will also need to be examined.

Parameterising scheduling possibilities

This project will explore how the VICE variant of VDM++ can be made more generic by adding more potential scheduling posibilities and if possible enable the user to specify his own scheduling algorithm to be used as one or more CPU's.

Measuring Embedded Distributed VICE models acuracy

This project will specify a real-time distributed system in VDM++ and implement the same system by hand in a programming language on alternative system architectures and then measure the acuracy of the bottlenecks predicted from the VICE model. This project will also explore how precise it is going to be possible to augment the VICE models using additional duration and cycles statements.

System wide timing analysis

This project will experiment with the analysis of timed event trace produced by the VICE interpreter starting with the work done in a paper for timing predicates from the HASE'07 conference. The main challenge here is to explore the predicate expressiveness needed for a number of case studies and then analysing the traces generated from exploring different scenarios using timed validation conjectures predicates expressed used that level of expressiveness.

Combining VDM++ with continuous time simulators

This project will take the PhD^? thesis of Marcel Verhoef as a starting point and explore ways of which one can combine models which are partly described in VDM++ and partly using a continuous time simulator. One or more case studies will be incorporated to examine the benefits of this kind of combination.

VDM++ supporting hardware/software co-design

This project will explore the possibilities for using VDM++ in a model-driven development context in the support for hardware/software co-design. This project will need to dig into the currently best approach to carry out hardware/software co-design and then explore whether the abstraction features and the precision from VDM++ may be able to augment that in a beneficial manner.

-- PeterGormLarsen - 23 Mar 2008