The Sixth VDM-Overture Workshop at Newcastle University

7-8 May 2009

The full picture album can be downloaded.

This workshop was organised at the University of Newcastle in the UK. The overall theme of this workshop was to exercise different aspects of developing software for the Overture open source platform on top of Eclipse. In order to compile the Overture executables different steps need to be taken to produce subprojects without the Eclipse interface or with the Eclipse interface. The aspects that will be covered included:

• Kernel functionality developed on top of the abstract syntax using VDM++ and with code generation to java
• User interface functionality focusing on how to develop Eclipse plug-ins
• Testing using VDMUnit and JUnit of Overture components.

The programme was:

7th May

• 08:30 – 09:00 Welcome, check internet access etc.
• 09:00 – 10:00 Introduction to Eclipse, creating Eclipse plug-ins and the Overture editor (David Møller)
• Break
• 10:30 – 11:00 Exercise with the Overture editor (David Møller)
• 11:00 – 12:00 Introduction to VDMJ (Nick Battle)
• Lunch
• 13:00 – 14:15 VDMJ continued and the VDMJ interpreter (Nick Battle)
• Break
• 14:30 – 16:00 Incorporating the VDMJ interpreter; Exercise (David Møller)
• Break
• 16:15 – 17:30 Calling external code from Eclipse; Exercise (David Møller)
• 17:30 – 18:00 Closing (Peter Gorm Larsen)
• 19:00 Workshop Dinner

8 May

• 9:00 - 11:00 Structure of Overture tool development; Exercise (Marcel Verhoef)
• Break
• 11:30 – 13:00 Introduction to the Overture kernel (Marcel Verhoef)
• Lunch
• 14:00 – 14:30 Overture UML mapper using the Overture kernel (Kenneth Lausdahl)
• 14:30 – 15:00 Overture proof obligation and export to HOL (Miguel Ferriera)
• 15:00 – 15:30 Combinatorial Testing Component (Kenneth Lausdahl & Peter Gorm Larsen)
• Break
• 15:45 – 16:30 The Maven plug-in for VDM models in Overture Exercise (Kenneth Lausdahl)
• 16:30 – 17:00 Closing Discussion (Peter Gorm Larsen)

During the workshop we came up with a list of outstanding issues that needs attension (in brackets the responsible persons are listed):

• Updatesite (David Møller and Christian Thillerman)
• Refactoring support (David Møller and Christian Thillerman)
• Auto-completion, intelisense (David Møller and Christian Thillerman)
• Debugger easier to use (David Møller and Christian Thillerman)
• Proof obligations transformed to proof engine (Miguel Ferriera)
• Pre-processed Eclipse with Overture installed for Windows, Linux and Mac platforms (Miguel Ferriera and Kenneth Lausdahl)
• Make the Maven eclipse part easier (Kenneth Lausdahl, David Møller and Christian Thillerman)
• Move Eclipse Maven stuff from Kenneths own pages to West Consulting (Kenneth Lausdahl and Marcel Verhoef) - Done
• Enabling navigation menu items on the side of overturetool.org web pages (Miguel Ferriera) - Done
• Overture documentation and getting started guide (to be reviewed by Peter Gorm Larsen and Nico Plat)
• Development guide for Overture developers (Kenneth Lausdahl)
• Check in sources of showtrace, ASTGen (Marcel Verhoef)
• Overture Java code generator based on library from VDMJ (not assigned but priority for next student project)
• Bug reporting/tracking set up (not assigned yet)
• One parser and one AST (not priority right now but Nick Battle, Marcel Verhoef and Peter Gorm Larsen will discuss)

-- PeterGormLarsen - 08 May 2009