Overture projects

From Wiki.overturetool.org

Background

Overture is an open-source project aimed at developing a comprehensive tool set for all VDM dialects 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 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. 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 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. Some extensions of this work have been carried out by Miguel Ferreira from Minho University in Portugal. The results of his work is impressive but much more work is needed on top of this in particular at the Eclipse GUI level.

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 or instrumenting PAT. 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. Currently there is an MSc thesis carried out by Maihemutijiang Maimaiti at Aarhus University on the automatic production of Java code from VDM++. However, there is room for additional work here.

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. An MSc project has previously been undertaken by Adriana Sucena from Minho University on an exchange to the Engineering College of Aarhus. Subsequently a small development team have refined this and developed a new version that is available as combinatorial testing in the Overture tool suite. This new MSc project would extend that work and explore possibilities for better filtering capabilities and higher lever of automation or doing different kinds of test automation.

Development of support for timing properties in VDM-RT (Master's level)

This project would take the Validation Support for Distributed Real-Time Embedded Systems in VDM++ paper from the HASE conference in 2007 as a starting point. The overall idea is to be able to express timing properties over timed traces in the form of VDM-RT logfiles and then have tool support that will be able to detect potential violations of such timing properties and visualise any violations in the VDM-RT logfile viewer. This project could also redevelop the VDM-RT logfile viewer so it would be more user friendly.

Development of Overture 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 IDE.

Coupling Overture to MDA and UML/SysML (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 and Enterprise Architect. This exploration should include a clarification whether any new features in UML2.0 with advantage can be exploited as well. An MSc thesis by Kenneth Lausdahl and Hans Kristian Lintrup from the Engineering College of Aarhus have been carried out some time ago. The new MSc project would take that as a starting point and extend it further with additional types of UML as well as SysML diagrams.

Coupling Statecharts with VDM (Master's level)

This project will take inspiration from the Practical Statecharts in C/C++ book and develop a framework in Overture/VDM that enables easy modelling of Statecharts using VDM. If possible this project shall also combine with the relevant part of UML tools enabling an automatic transformation from a graphical Statecharts representation into this new VDM framework.

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. A precurser of this project have been undertaken by Carlos Vilhena from Minho University on an exchange to the Engineering College of Aarhus until summer 2008. This project would extend that work and make it more usable for a large subset of the languages.

Slicing support for VDM (Master's level)

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.

Adding dynamic deployment to CPUs for VDM-RT (Master's level)

This project aims at exploring how dynamic deployment of functionality to CPUs in the VDM-RT dialect both theoretically as well as in the Overture platform. A small case study will also be used to examine how well the extension will work in practice. This project is currently undertaken by Claus Ballegaard Nielsen at Aarhus University/IHA until December 2010.

Deadlock analysis for VDM++ (Master's level)

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 (Master's level)

This project will explore how the VDM-RTvariant 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 VDM-RT models acuracy (Master's level)

This project will specify a real-time distributed system in VDM-RT 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 VDM-RT model. This project will also explore how precise it is going to be possible to augment the VDM-RT models using additional duration and cycles statements.

Experimenting with combining VDM-RT with continuous time simulators (Master's level)

This project will take the PhD thesis of Marcel Verhoef and the prototype of the co-simulation engine from the DESTECS project 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-RT Memory analysis (Master's level)

This project will explorer how the VDM-RT is interpreted in terms for memory usage. First semantics for the VDM-RT memory model must be defined to enable future analysis. The main challenge is to define a mapping from the VDM memory model to a memory model which can be compared with a hardware configuration. The project should aim to develop a technique to compare a VDM model to a hardware configuration much in the same way as in the VDM-RT project.

Development of test regression environment for Overture (Bachelor's level)

This project will focus on extending the existing test regression environment for the Overture environment both in the detailed core functional components (parsers, type checker, interpreter, proof obligation generator) as well as automation of the GUI testing in a regression fashion. Test coverage at the source Java level shall be extended in the best possible ways.

Additional Potential Projects for "Technical IT" students at Aarhus University

In addition to the Overture tasks proposed above the Modelling and Validation of Critical Systems group at Aarhus School of Engineering lead by Peter Gorm Larsen offer the following additional MSc projects:

Creating a VDM model of Turning Static Process Descriptions Dynamic (Master's level)

This project should be carried out at Masters level and in collaboration with the Callis company in close relation with an ongoing research project with this theme. Currently Callis has tools called Author and Performer and these can be used to describe the processes used for development at a company in a static fashion. The intend of the project here is to be able to produce dynamic overview of each project following the process by extracting information from internal resources and presenting these to different stakeholders. This project can also include actual implementation of some of these aspects.

Modelling and validation of Multimedie control protocol (Master's level)

This project is carried out in collaboration with Bang & Olufsen and the intend is to model the protocol using VDM and validate its appropriate behaviour by producing a collection of test cases that can be used with the model. Extensions of the existing ideas for the protocol such as connection with DNLA shall be examined in order to determine its extendability.

Evaluating Usefullness of Test Automation Tools such as PEX (Master's level)

This project will evaluate the usefullness of test automation tools such as the PEX tool from Microsoft. The evaluation shall look at alternative tools as well and come up with recommendations for how this kind of tools can share information with other tools about the information derived and how to best communicate the findings to the users.

Overview of System of Systems Technologies (Master's level)

This project will explore the existing litterature and tools supporting a System of Systems (SoS) development. This will include notations such as AADL and SysML but will also explore on the analysis that can be conducted for this kind of SoS development.

Evaluating of Executable UML models (Master's level)

This project will examine fUML and xUML and experiment with using these for a case study that. The evaluation shall evaluate pros and cons of using this kind of technology and come with advice about how this kind of technology potentially can be combined with a formalism such as VDM.

Comparison of different specification formalisms and tool support (Master's level)

This project will take a case study and try to model it using different specification formalism and associated tools and based on this provide recommendations about pros and cons for such different technologies. The formalisms to be considered here could for example include VDM, Z, B, CCS, CSP, Circus, OBJ, Maude, RAISE.

Updating Home Automation Front End for User Friendliness (BSc or Master's level)

This project will take the user interface comming out of the "Minimum Comfiguration - Home Automation" (MC-HA) project such that it will become more user friendly. Subsequently it shall be attempted to use this as a frontend to a similar home automation engine from Qees.