Overture Master theses
From Wiki.overturetool.org
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 final 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.
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.
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.
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 first 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.
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.
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.
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.
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.
Dynamic Reconfiguration of Distributed Systems in VDM-RT (Claus Ballegård Nielsen, Århus, December 2010)
Abstract: Nowadays computers are found everywhere and with an ever increasing functionality. More and more of them exist in cooperative networks with other computers in order to form distributed systems. These systems often have high demands for adaptability and scalability which means that they are expected to adapt to requirements that are characterized by constant change. This can be achieved through a dynamic behavior in which the system has the ability to adapt to system modification by the means of dynamic reconfiguration. However as the possibilities in software increase, so does the complexity of system specifications and designs, making development of distributed systems increasingly challenging. VDM-RT is a modeling language used to validate and verify software through the entire software development process, with a particular focus on distributed systems. In the existing VDM-RT language the architecture of the distributed systems is preconfigured in the model and it stays static throughout the execution of the model. This thesis has evaluated the feasibility and value of extending VDM-RT with dynamic reconfiguration in order to facilitate the modeling of dynamic distributed systems and the validation of subsequent implementations. Common principles of dynamic reconfiguration have been examined and the existing literature has been evaluated to form a foundation for an extension of VDM-RT. The result is a well-founded language extension, with defined semantics, for expressing dynamic reconfiguration in VDM-RT, as well as the development of a interpreter prototype and the successful application of the extension into two case studies.
Towards Development of Overture/VDM++ to Java Code Generator (Maihemutijiang Maimaiti, Århus, June 2011)
Abstract: User requirements are usually stated in an informal way in the form of a natural language and graphical illustrations. A good modelling method enables software developers to formalize the requirements in a better way so that the ideas behind the envisaged system can be validated before implementing it in a programming language. As a formal method, VDM++ models the system in mathematically strict (formal) way and uses rigorous notation which has the desired features and gives the possibility that part of the implementation process of the system in a programming language can be automated. The automatic code generation can potentially reduce the cost of implementation. Furthermore, the generated code will then have a direct and strong conformance to its high-level specification (a VDM++ model) which has strong correspondence with the user requirements. Since VDM++ is object-oriented, it is reasonable to generate codes in an object-oriented programming language. In this context, Java is chosen to be the implementation programming language for it is currently one of the most prominent object-oriented languages. This thesis investigates mapping possibilities from VDM++ constructs to Java and describes the design and development of a Java code generator from VDM++ specification.
A VDM-RT Methodology for the HW/SW Co-design of Embedded Systems (José Antonio Esparza Isasa, Århus, December 2011)
Abstract: This thesis presents a new methodology for Hardware/Software Co-design of embedded systems. The proposed methodology is based on the modelling language VDM-RT. This new approach allows system engineers to perform design space exploration at an abstract level earlier in the development process. This methodology supports the analysis of real-time deadlines under different hardware/software architectures, without making use of virtual or actual prototyping. Based on the information gained during this analysis, system engineers are able to allocate the required system functionality in hardware and software blocks. This allocation or partitioning process can be done through a rigorous study of the design trade-offs by applying the VDM-RT methodology. As an additional advantage, the system engineers are able to specify and capture clearly and unambiguously the system structure and behaviour. Besides presenting this new methodology, this thesis will show its application in two case studies and present a pragmatic analysis of its performance.
