Overture Publications

Master Theses

The Overture Project - Designing an open source tool set (Pieter van der Spek, Delft, August 2004)

Abstract: Overture is a formal modeling method that is currently being developed. This thesis describes the process of the design and implementation of a development environment for the Overture Modeling Language which is part of Overture. The set of tools that is the result of this efort consists of three components. The first and most visible component is a front-end, integrated in the Eclipse Platform. This front-end consists of an editor and some functionality to supply information to the user (e.g. error messages). The second part is a compiler. This part handles the verifcation of the syntax and the semantics of the user input. The third and nal part consists of an XML processor. This part transforms the original user input into an XML representation. Also, the processor is able to validate the XML representation with the help of an XML Schema.

• TheOvertureProjectDesigningOpenSourceToolSet.pdf: The Overture Project - Designing an Open Source Tool Set

Development of an Overture/VDM++ Tool Set for Eclipse (Jacob Porsborg Nielsen and Jens Kielsgaard Hansen, Lyngby, August 2005)

Abstract: In this project a kernel for an Overture Tool Set supporting OML (Overture Modelling Language) has been developed. OML is very similar to the formal specification language VDM++. The Overture Tool Set is based on the Eclipse framework, which means that the tools integrate with an Eclipse based editor. The kernel provides functionality for parsing an OML specification and storing the information in an AST (Abstract Syntax Tree), reconstructing source code from the AST, and importing and exporting this AST representation to XML. The kernel is extensible so that further functionality can be added to the Overture Tool Set without changing the kernel implementation. This feature is implemented using the plug-in structure of Eclipse and Visitor Design Patterns. Furthermore, three ’proof of concept’ plug-ins have been developed – one for exporting a simple OML specification to an UML class diagram, one for importing a simple UML class diagram to OML, and one to show that the kernel can handle refactoring of an AST. The report documents analysis, design, implementation, test, and how the kernel can be extended.

• IMM-THESIS-2005-58.pdf: Development of an Overture/VDM++ Tool Set for Eclipse

Extending the VDM++ formal specification language with type inference and generic classes (Thomas Christensen, Aarhus, April 2007)

Abstract This thesis is divided into three phases. In the first phase, we convert a VDMSL specification of a VDM++ static semantics checker to VDM++. Apart from the translation, we introduce a new architecture for the static semantics checker based on automatically generated AST visitors. The second phase is an study of the feasability of extending OML with two new language feature, implicitly-typed functions and Java-style generic classes. Finally in the third phase, we provide a proof of concept of type-inference of implicitly-typed functions for a small subset of OML and a partial implementation of Generic classes.

• Thomas_Christensen_thesis.pdf: Extending the VDM++ formal specification language with type inference and generic classes

Automatically Discharging VDM Proof Obligations using HOL (Sander Vermolen, Aarhus/Nijmegen, August 2007)

Abstract: Statically undecidable inconsistencies in VDM++ models can result in runtime errors when executing the model. The absence of these inconsistencies can be verified by proving the corresponding proof obligation to be valid. This thesis comprises two main steps. The rst is a translation of functional VDM++ models to semantically equivalent HOL models. The second is an automated proof of the obligations that are generated from a VDM++ model. The combination of these two steps can ensure consistency of the model and thereby stability of the execution.

• ThesisSanderVermolen.pdf: Automatically Discharging VDM Proof Obligations using HOL

Connecting between VDM++ and JML (Carlos Vilhena, Århus/Minho, July 2008)

Abstract: This thesis aims to discuss a number of possibilities for automatic connection between VDM++ and JML, in both directions The project aims at identifying the possible subsets for which this connection is possible, as well as describing in detail all the imitations encountered. It is believed that such a connection can enable VDM++ to act as a front-end for contract-based programming, the usage of tool support from both sides and can allow different teaching perspectives with respect to formal methods. The development of a prototype proof-of-concept implementation of this bi-directional mapper based on its possible theoretical limitations is the mail goal of this work.

• ConnectingVDMppJML.pdf: Connecting between VDM++ and JML

VDM++ Test Automation Support (Adriana Sucena, Århus/Minho, July 2008)

Abstract: Testing is an important, expensive, repetitive and exhaustive task in software development. It does not guarantee that any kind of model has no errors, how ever the developer can be more confident that a model is working properly after testing it. If the testing process is done along the development, it will have to be frequently repeated because a small change in the model might influence its behaviour. Repeating tests, without automation support, each time a change is made is a tedious manual task. It is also time consuming and, consequently, expensive. In this thesis, it is suggested theoretical and practical approaches of test automation in VDM++. The main goal is to contribute to reduce the effort VDM++ users need to spend to test VDM++ models.

• VDMppTestAutomationSupport.pdf: VDM++ Test Automation Support

Coupling Overture to MDA and UML (Kenneth Lausdahl and Hans Kristian Lintrup, Århus, December 2008)

Abstract: It is vital that critical software systems perform as intended. An effective way to minimize the risk of unforeseen surprises in a system is to create a model of the system's critical parts. VDM++ is an OO modeling language used to validate and verify the design of software systems at a desired level of abstraction. VDMTools is a toolset which offers various features to support software development based on VDM and its predecessor, VDM-SL. Among the features offered by VDMTools, is the Rose-VDM++ Link which enables going back and forth between VDM++ model and UML version 1.1. This M.Sc. thesis presents an analysis of the additional possibilities offered by UML version 2. The results of this are materialized as an extension of the Overture project which is a community-based project dedicated to the development of the next generation of tools supporting formal modeling and analysis in the design of software systems. We have developed a counterpart to the Rose-VDM++ Link, i.e. a tool for going back and forth between VDM++ models and UML 2.0 Class Diagrams and Sequence Diagrams.

• COMU.pdf: Coupling Overture to MDA and UML

Using Eclipse for Exploring an Integration Architecture for VDM (David Møller and Christian Thillermann, Århus, June 2009)

Abstract: For many years academics have agitated for the use of formal methods in software development, arguing that it is an effective remedy for low quality of software and a method for detecting defects earlier, decreasing rework and automating property checking. The industry in general however has been reluctant to adopt the use of formal methods. The lack of adequate tool support has been proposed as one of the most important reasons for this. While there also may be other reasons, this thesis seeks to accommodate the need for adequate tool support by investigation of the possibilities for developing an IDE for VDM development. VDM is one of the oldest and most mature formal methods available. IDEs for established programming languages such as Java, C++, C# etc. provide a comprehensive set of features aiding the developers in their work. For VDM such functionality is unavailable. Eclipse is a widely used software development platform that offers a plug-in system, allowing extension of existing functionality. Eclipse will be used as the platform for an IDE comprising editor, parser, type checker and debugger and integration of available VDM tools. Thus providing a common interface for VDM development. The work of this thesis is part of the Overture open source initiative.

• UsingEclipseExploringIntegrationArchitectureVDM.PDF: Using Eclipse for Exploring an Integration Architecture for VDM

-- PeterGormLarsen - 08 Jun 2009